System Description: RDL Rewrite and Decision Procedure Laboratory
Identifieur interne : 003569 ( Istex/Corpus ); précédent : 003568; suivant : 003570System Description: RDL Rewrite and Decision Procedure Laboratory
Auteurs : Alessandro Armando ; Luca Compagna ; Silvio RaniseSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: RDL1 simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and Simplify [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows: 1 RDL is based on CCR (Constraint Contextual Rewriting) [1 2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic. 2 RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers ‘plug-and-play’ decision procedures for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13]. 3 RDL implements instances of a generic extension schema for decision procedures [3]. The key ingredient of such a schema is a lemma speculation mechanism which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, affinization is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a combination of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).
Url:
DOI: 10.1007/3-540-45744-5_54
Links to Exploration step
ISTEX:E11AF6385D5BFE96BFA4FA03092EC0A43FF766E7Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">System Description: RDL Rewrite and Decision Procedure Laboratory</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><affiliation><mods:affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: armando@dist.unige.it</mods:affiliation></affiliation></author><author><name sortKey="Compagna, Luca" sort="Compagna, Luca" uniqKey="Compagna L" first="Luca" last="Compagna">Luca Compagna</name><affiliation><mods:affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: compa@dist.unige.it</mods:affiliation></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation><mods:affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA-INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101, 54602, Villers les Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: silviog@dist.unige.it</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E11AF6385D5BFE96BFA4FA03092EC0A43FF766E7</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45744-5_54</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-J27HB5TV-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003569</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003569</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">System Description: RDL Rewrite and Decision Procedure Laboratory</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><affiliation><mods:affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: armando@dist.unige.it</mods:affiliation></affiliation></author><author><name sortKey="Compagna, Luca" sort="Compagna, Luca" uniqKey="Compagna L" first="Luca" last="Compagna">Luca Compagna</name><affiliation><mods:affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: compa@dist.unige.it</mods:affiliation></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation><mods:affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA-INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101, 54602, Villers les Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: silviog@dist.unige.it</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: RDL1 simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and Simplify [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows: 1 RDL is based on CCR (Constraint Contextual Rewriting) [1 2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic. 2 RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers ‘plug-and-play’ decision procedures for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13]. 3 RDL implements instances of a generic extension schema for decision procedures [3]. The key ingredient of such a schema is a lemma speculation mechanism which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, affinization is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a combination of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Alessandro Armando</name><affiliations><json:string>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</json:string><json:string>E-mail: armando@dist.unige.it</json:string></affiliations></json:item><json:item><name>Luca Compagna</name><affiliations><json:string>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</json:string><json:string>E-mail: compa@dist.unige.it</json:string></affiliations></json:item><json:item><name>Silvio Ranise</name><affiliations><json:string>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</json:string><json:string>LORIA-INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101, 54602, Villers les Nancy Cedex, France</json:string><json:string>E-mail: silviog@dist.unige.it</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-J27HB5TV-1</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: RDL1 simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and Simplify [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows: 1 RDL is based on CCR (Constraint Contextual Rewriting) [1 2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic. 2 RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers ‘plug-and-play’ decision procedures for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13]. 3 RDL implements instances of a generic extension schema for decision procedures [3]. The key ingredient of such a schema is a lemma speculation mechanism which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, affinization is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a combination of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).</abstract><qualityIndicators><score>8.091</score><pdfWordCount>3091</pdfWordCount><pdfCharCount>16396</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>7</pdfPageCount><pdfPageSize>430 x 650 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>435</abstractWordCount><abstractCharCount>2899</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>System Description: RDL Rewrite and Decision Procedure Laboratory</title><chapterId><json:string>54</json:string><json:string>Chap54</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2001</copyrightDate><issn><json:string>0302-9743</json:string></issn><editor><json:item><name>G. Goos</name></json:item><json:item><name>J. Hartmanis</name></json:item><json:item><name>J. van Leeuwen</name></json:item></editor></serie><host><title>Automated Reasoning</title><language><json:string>unknown</json:string></language><copyrightDate>2001</copyrightDate><doi><json:string>10.1007/3-540-45744-5</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-45744-2</json:string></eisbn><bookId><json:string>3-540-45744-5</json:string></bookId><isbn><json:string>978-3-540-42254-9</json:string></isbn><volume>2083</volume><pages><first>663</first><last>669</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Rajeev Goré</name><affiliations><json:string>Automated Reasoning Project and Department of Computer Science, Australian National University, 0200, Canberra, ACT, Australia</json:string><json:string>E-mail: Rajeev.Gore@arp.anu.edu.au</json:string></affiliations></json:item><json:item><name>Alexander Leitsch</name><affiliations><json:string>AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria</json:string><json:string>E-mail: leitsch@logic.at</json:string></affiliations></json:item><json:item><name>Tobias Nipkow</name><affiliations><json:string>Institut für Informatik, Technische Universität München, 80290, München, Germany</json:string><json:string>E-mail: nipkow@in.tum.de</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Mathematical Logic and Foundations</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-J27HB5TV-1</json:string></ark><publicationDate>2001</publicationDate><copyrightDate>2001</copyrightDate><doi><json:string>10.1007/3-540-45744-5_54</json:string></doi><id>E11AF6385D5BFE96BFA4FA03092EC0A43FF766E7</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-J27HB5TV-1/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-J27HB5TV-1/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-J27HB5TV-1/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">System Description: RDL Rewrite and Decision Procedure Laboratory</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2001">2001</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">System Description: RDL Rewrite and Decision Procedure Laboratory</title><author><persName><forename type="first">Alessandro</forename><surname>Armando</surname></persName><email>armando@dist.unige.it</email><affiliation><orgName type="institution">DIST-Università degli Studi di Genova</orgName><address><street>via all’Opera Pia 13</street><postCode>16145</postCode><settlement>Genova</settlement><country key="IT">ITALY</country></address></affiliation></author><author><persName><forename type="first">Luca</forename><surname>Compagna</surname></persName><email>compa@dist.unige.it</email><affiliation><orgName type="institution">DIST-Università degli Studi di Genova</orgName><address><street>via all’Opera Pia 13</street><postCode>16145</postCode><settlement>Genova</settlement><country key="IT">ITALY</country></address></affiliation></author><author><persName><forename type="first">Silvio</forename><surname>Ranise</surname></persName><email>silviog@dist.unige.it</email><affiliation><orgName type="institution">DIST-Università degli Studi di Genova</orgName><address><street>via all’Opera Pia 13</street><postCode>16145</postCode><settlement>Genova</settlement><country key="IT">ITALY</country></address></affiliation><affiliation><orgName type="institution">LORIA-INRIA-Lorraine</orgName><address><street>615, rue du Jardin Botanique</street><postBox>BP 101</postBox><postCode>54602</postCode><settlement>Villers les Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">E11AF6385D5BFE96BFA4FA03092EC0A43FF766E7</idno><idno type="ark">ark:/67375/HCB-J27HB5TV-1</idno><idno type="DOI">10.1007/3-540-45744-5_54</idno></analytic><monogr><title level="m" type="main">Automated Reasoning</title><title level="m" type="sub">First International Joint Conference, IJCAR 2001 Siena, Italy, June 18–22, 2001 Proceedings</title><title level="m" type="part">Automata, Specification, Verification, and Logics of Programs</title><idno type="DOI">10.1007/3-540-45744-5</idno><idno type="book-id">3-540-45744-5</idno><idno type="ISBN">978-3-540-42254-9</idno><idno type="eISBN">978-3-540-45744-2</idno><idno type="chapter-id">Chap54</idno><idno type="part-id">Part25</idno><editor><persName><forename type="first">Rajeev</forename><surname>Goré</surname></persName><email>Rajeev.Gore@arp.anu.edu.au</email><affiliation><orgName type="department">Automated Reasoning Project and Department of Computer Science</orgName><orgName type="institution">Australian National University</orgName><address><settlement>Canberra</settlement><region>ACT</region><postCode>0200</postCode><country key="AU">AUSTRALIA</country></address></affiliation></editor><editor><persName><forename type="first">Alexander</forename><surname>Leitsch</surname></persName><email>leitsch@logic.at</email><affiliation><orgName type="department">AG Theoretische Informatik und Logik, Institut für Computersprachen</orgName><orgName type="institution">Technische Universität Wien</orgName><address><street>Favoritenstr. 9, E185-2</street><postCode>1040</postCode><settlement>Wien</settlement><country key="AT">AUSTRIA</country></address></affiliation></editor><editor><persName><forename type="first">Tobias</forename><surname>Nipkow</surname></persName><email>nipkow@in.tum.de</email><affiliation><orgName type="department">Institut für Informatik</orgName><orgName type="institution">Technische Universität München</orgName><address><postCode>80290</postCode><settlement>München</settlement><country key="DE">GERMANY</country></address></affiliation></editor><imprint><biblScope unit="vol">2083</biblScope><biblScope unit="page" from="663">663</biblScope><biblScope unit="page" to="669">669</biblScope><biblScope unit="chapter-count">59</biblScope><biblScope unit="part-chapter-count">7</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">G.</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><editor><persName><forename type="first">J.</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName></editor><idno type="pISSN">0302-9743</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>RDL<hi rend="superscript">1</hi> simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and <hi rend="italic">Simplify</hi> [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows:
<list type="ordered"><item n="1"><p>RDL is based on CCR (Constraint Contextual Rewriting) [1
2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic.</p></item><item n="2"><p>RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers <hi rend="italic">‘plug-and-play’ decision procedures</hi> for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13].</p></item><item n="3"><p>RDL implements instances of a <hi rend="italic">generic extension schema</hi> for decision procedures [3]. The key ingredient of such a schema is a <hi rend="italic">lemma speculation mechanism</hi> which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, <hi rend="italic">affinization</hi> is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a <hi rend="italic">combination</hi> of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).</p></item></list></p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I21017</label><item><term type="Secondary" subtype="priority-1">Artificial Intelligence (incl. Robotics)</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-2">Mathematical Logic and Formal Languages</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-3">Logics and Meanings of Programs</term></item><label>I14029</label><item><term type="Secondary" subtype="priority-4">Software Engineering</term></item><label>M24005</label><item><term type="Secondary" subtype="priority-5">Mathematical Logic and Foundations</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-J27HB5TV-1/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-45744-5</BookID><BookTitle>Automated Reasoning</BookTitle><BookSubTitle>First International Joint Conference, IJCAR 2001 Siena, Italy, June 18–22, 2001 Proceedings</BookSubTitle><BookVolumeNumber>2083</BookVolumeNumber><BookSequenceNumber>2083</BookSequenceNumber><BookDOI>10.1007/3-540-45744-5</BookDOI><BookTitleID>69372</BookTitleID><BookPrintISBN>978-3-540-42254-9</BookPrintISBN><BookElectronicISBN>978-3-540-45744-2</BookElectronicISBN><BookChapterCount>59</BookChapterCount><BookHistory><OnlineDate><Year>2001</Year><Month>6</Month><Day>8</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2001</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I14029" Priority="4" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="M24005" Priority="5" Type="Secondary">Mathematical Logic and Foundations</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Rajeev</GivenName><FamilyName>Goré</FamilyName></EditorName><Contact><Email>Rajeev.Gore@arp.anu.edu.au</Email></Contact></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Alexander</GivenName><FamilyName>Leitsch</FamilyName></EditorName><Contact><Email>leitsch@logic.at</Email></Contact></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Tobias</GivenName><FamilyName>Nipkow</FamilyName></EditorName><Contact><Email>nipkow@in.tum.de</Email></Contact></Editor><Affiliation ID="Aff1"><OrgDivision>Automated Reasoning Project and Department of Computer Science</OrgDivision><OrgName>Australian National University</OrgName><OrgAddress><City>Canberra</City><State>ACT</State><Postcode>0200</Postcode><Country>Australia</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>AG Theoretische Informatik und Logik, Institut für Computersprachen</OrgDivision><OrgName>Technische Universität Wien</OrgName><OrgAddress><Street>Favoritenstr. 9, E185-2</Street><Postcode>1040</Postcode><City>Wien</City><Country>Austria</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgDivision>Institut für Informatik</OrgDivision><OrgName>Technische Universität München</OrgName><OrgAddress><Postcode>80290</Postcode><City>München</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part25"><PartInfo TocLevels="0"><PartID>25</PartID><PartSequenceNumber>25</PartSequenceNumber><PartTitle>Automata, Specification, Verification, and Logics of Programs</PartTitle><PartChapterCount>7</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-45744-5</BookID><BookTitle>Automated Reasoning</BookTitle></PartContext></PartInfo><Chapter ID="Chap54" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>54</ChapterID><ChapterDOI>10.1007/3-540-45744-5_54</ChapterDOI><ChapterSequenceNumber>54</ChapterSequenceNumber><ChapterTitle Language="En">System Description: RDL Rewrite and Decision Procedure Laboratory</ChapterTitle><ChapterFirstPage>663</ChapterFirstPage><ChapterLastPage>669</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2001</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2001</Year><Month>6</Month><Day>7</Day></RegistrationDate><OnlineDate><Year>2001</Year><Month>6</Month><Day>8</Day></OnlineDate></ChapterHistory><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>25</PartID><BookID>3-540-45744-5</BookID><BookTitle>Automated Reasoning</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Alessandro</GivenName><FamilyName>Armando</FamilyName></AuthorName><Contact><Email>armando@dist.unige.it</Email></Contact></Author><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Luca</GivenName><FamilyName>Compagna</FamilyName></AuthorName><Contact><Email>compa@dist.unige.it</Email></Contact></Author><Author AffiliationIDS="Aff6 Aff7"><AuthorName DisplayOrder="Western"><GivenName>Silvio</GivenName><FamilyName>Ranise</FamilyName></AuthorName><Contact><Email>silviog@dist.unige.it</Email></Contact></Author><Affiliation ID="Aff6"><OrgName>DIST-Università degli Studi di Genova</OrgName><OrgAddress><Street>via all’Opera Pia 13</Street><Postcode>16145</Postcode><City>Genova</City><Country>Italy</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>LORIA-INRIA-Lorraine</OrgName><OrgAddress><Street>615, rue du Jardin Botanique</Street><Postbox>BP 101</Postbox><Postcode>54602</Postcode><City>Villers les Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>RDL<Superscript>1</Superscript> simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and <Emphasis Type="Italic">Simplify</Emphasis> [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows:
<OrderedList><ListItem><ItemNumber>1</ItemNumber><ItemContent><Para>RDL is based on CCR (Constraint Contextual Rewriting) [1
2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic.</Para></ItemContent></ListItem><ListItem><ItemNumber>2</ItemNumber><ItemContent><Para>RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers <Emphasis Type="Italic">‘plug-and-play’ decision procedures</Emphasis> for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13].</Para></ItemContent></ListItem><ListItem><ItemNumber>3</ItemNumber><ItemContent><Para>RDL implements instances of a <Emphasis Type="Italic">generic extension schema</Emphasis> for decision procedures [3]. The key ingredient of such a schema is a <Emphasis Type="Italic">lemma speculation mechanism</Emphasis> which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, <Emphasis Type="Italic">affinization</Emphasis> is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a <Emphasis Type="Italic">combination</Emphasis> of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).</Para></ItemContent></ListItem></OrderedList></Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle><SubSeriesSubTitle Language="En">Subseries of Lecture Notes in Computer Science</SubSeriesSubTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Jö</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff4"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saabrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>System Description: RDL Rewrite and Decision Procedure Laboratory</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>System Description: RDL Rewrite and Decision Procedure Laboratory</title></titleInfo><name type="personal"><namePart type="given">Alessandro</namePart><namePart type="family">Armando</namePart><affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</affiliation><affiliation>E-mail: armando@dist.unige.it</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Luca</namePart><namePart type="family">Compagna</namePart><affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</affiliation><affiliation>E-mail: compa@dist.unige.it</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Silvio</namePart><namePart type="family">Ranise</namePart><affiliation>DIST-Università degli Studi di Genova, via all’Opera Pia 13, 16145, Genova, Italy</affiliation><affiliation>LORIA-INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101, 54602, Villers les Nancy Cedex, France</affiliation><affiliation>E-mail: silviog@dist.unige.it</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2001</dateIssued><copyrightDate encoding="w3cdtf">2001</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: RDL1 simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and Simplify [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows: 1 RDL is based on CCR (Constraint Contextual Rewriting) [1 2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic. 2 RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers ‘plug-and-play’ decision procedures for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13]. 3 RDL implements instances of a generic extension schema for decision procedures [3]. The key ingredient of such a schema is a lemma speculation mechanism which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, affinization is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a combination of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).</abstract><relatedItem type="host"><titleInfo><title>Automated Reasoning</title><subTitle>First International Joint Conference, IJCAR 2001 Siena, Italy, June 18–22, 2001 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Rajeev</namePart><namePart type="family">Goré</namePart><affiliation>Automated Reasoning Project and Department of Computer Science, Australian National University, 0200, Canberra, ACT, Australia</affiliation><affiliation>E-mail: Rajeev.Gore@arp.anu.edu.au</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Alexander</namePart><namePart type="family">Leitsch</namePart><affiliation>AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria</affiliation><affiliation>E-mail: leitsch@logic.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Tobias</namePart><namePart type="family">Nipkow</namePart><affiliation>Institut für Informatik, Technische Universität München, 80290, München, Germany</affiliation><affiliation>E-mail: nipkow@in.tum.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2001</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="M24005">Mathematical Logic and Foundations</topic></subject><identifier type="DOI">10.1007/3-540-45744-5</identifier><identifier type="ISBN">978-3-540-42254-9</identifier><identifier type="eISBN">978-3-540-45744-2</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">69372</identifier><identifier type="BookID">3-540-45744-5</identifier><identifier type="BookChapterCount">59</identifier><identifier type="BookVolumeNumber">2083</identifier><identifier type="BookSequenceNumber">2083</identifier><identifier type="PartChapterCount">7</identifier><part><date>2001</date><detail type="part"><title>Automata, Specification, Verification, and Logics of Programs</title></detail><detail type="volume"><number>2083</number><caption>vol.</caption></detail><extent unit="pages"><start>663</start><end>669</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2001</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2001</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title><subTitle>Subseries of Lecture Notes in Computer Science</subTitle></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Rajeev</namePart><namePart type="family">Goré</namePart><affiliation>Automated Reasoning Project and Department of Computer Science, Australian National University, 0200, Canberra, ACT, Australia</affiliation><affiliation>E-mail: Rajeev.Gore@arp.anu.edu.au</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Alexander</namePart><namePart type="family">Leitsch</namePart><affiliation>AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria</affiliation><affiliation>E-mail: leitsch@logic.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Tobias</namePart><namePart type="family">Nipkow</namePart><affiliation>Institut für Informatik, Technische Universität München, 80290, München, Germany</affiliation><affiliation>E-mail: nipkow@in.tum.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jö</namePart><namePart type="family">Siekmann</namePart><affiliation>University of Saarland, Saabrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2001</recordOrigin></recordInfo></relatedItem><identifier type="istex">E11AF6385D5BFE96BFA4FA03092EC0A43FF766E7</identifier><identifier type="ark">ark:/67375/HCB-J27HB5TV-1</identifier><identifier type="DOI">10.1007/3-540-45744-5_54</identifier><identifier type="ChapterID">54</identifier><identifier type="ChapterID">Chap54</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2001</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2001</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-J27HB5TV-1/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003569 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003569 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:E11AF6385D5BFE96BFA4FA03092EC0A43FF766E7
|texte= System Description: RDL Rewrite and Decision Procedure Laboratory
}}
| This area was generated with Dilib version V0.6.33. |  |