A Model-Based Completeness Proof of Extended Narrowing and Resolution
Identifieur interne : 003966 ( Istex/Corpus ); précédent : 003965; suivant : 003967A Model-Based Completeness Proof of Extended Narrowing and Resolution
Auteurs : Jürgen StuberSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.
Url:
DOI: 10.1007/3-540-45744-5_15
Links to Exploration step
ISTEX:F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Model-Based Completeness Proof of Extended Narrowing and Resolution</title><author><name sortKey="Stuber, Jurgen" sort="Stuber, Jurgen" uniqKey="Stuber J" first="Jürgen" last="Stuber">Jürgen Stuber</name><affiliation><mods:affiliation>INRIA LORIA, 615 Rue Jardin Botanique, 54600, Villers-les-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: stuber@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45744-5_15</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-0496HD24-7/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003966</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003966</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Model-Based Completeness Proof of Extended Narrowing and Resolution</title><author><name sortKey="Stuber, Jurgen" sort="Stuber, Jurgen" uniqKey="Stuber J" first="Jürgen" last="Stuber">Jürgen Stuber</name><affiliation><mods:affiliation>INRIA LORIA, 615 Rue Jardin Botanique, 54600, Villers-les-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: stuber@loria.fr</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: We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Jürgen Stuber</name><affiliations><json:string>INRIA LORIA, 615 Rue Jardin Botanique, 54600, Villers-les-Nancy, France</json:string><json:string>E-mail: stuber@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-0496HD24-7</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>135</abstractWordCount><abstractCharCount>913</abstractCharCount><keywordCount>0</keywordCount><score>8.62</score><pdfWordCount>7004</pdfWordCount><pdfCharCount>32251</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>16</pdfPageCount><pdfPageSize>430 x 650 pts</pdfPageSize></qualityIndicators><title>A Model-Based Completeness Proof of Extended Narrowing and Resolution</title><chapterId><json:string>15</json:string><json:string>Chap15</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>195</first><last>210</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-0496HD24-7</json:string></ark><publicationDate>2001</publicationDate><copyrightDate>2001</copyrightDate><doi><json:string>10.1007/3-540-45744-5_15</json:string></doi><id>F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36</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-0496HD24-7/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-0496HD24-7/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-0496HD24-7/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">A Model-Based Completeness Proof of Extended Narrowing and Resolution</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">A Model-Based Completeness Proof of Extended Narrowing and Resolution</title><author><persName><forename type="first">Jürgen</forename><surname>Stuber</surname></persName><email>stuber@loria.fr</email><affiliation><orgName type="institution">INRIA LORIA</orgName><address><street>615 Rue Jardin Botanique</street><postCode>54600</postCode><settlement>Villers-les-Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36</idno><idno type="ark">ark:/67375/HCB-0496HD24-7</idno><idno type="DOI">10.1007/3-540-45744-5_15</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">A Model-Based Completeness Proof of Extended Narrowing and Resolution</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">Chap15</idno><idno type="part-id">Part12</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="195">195</biblScope><biblScope unit="page" to="210">210</biblScope><biblScope unit="chapter-count">59</biblScope><biblScope unit="part-chapter-count">1</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>We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.</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-0496HD24-7/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="Part12"><PartInfo TocLevels="0"><PartID>12</PartID><PartSequenceNumber>12</PartSequenceNumber><PartTitle>A Model-Based Completeness Proof of Extended Narrowing and Resolution</PartTitle><PartChapterCount>1</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-45744-5</BookID><BookTitle>Automated Reasoning</BookTitle></PartContext></PartInfo><Chapter ID="Chap15" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>15</ChapterID><ChapterDOI>10.1007/3-540-45744-5_15</ChapterDOI><ChapterSequenceNumber>15</ChapterSequenceNumber><ChapterTitle Language="En">A Model-Based Completeness Proof of Extended Narrowing and Resolution</ChapterTitle><ChapterFirstPage>195</ChapterFirstPage><ChapterLastPage>210</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>12</PartID><BookID>3-540-45744-5</BookID><BookTitle>Automated Reasoning</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Jürgen</GivenName><FamilyName>Stuber</FamilyName></AuthorName><Contact><Email>stuber@loria.fr</Email><URL>http://www.loria.fr/~stuber</URL></Contact></Author><Affiliation ID="Aff6"><OrgName>INRIA LORIA</OrgName><OrgAddress><Street>615 Rue Jardin Botanique</Street><Postcode>54600</Postcode><City>Villers-les-Nancy</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.</Para></Abstract><ArticleNote Type="Misc"><Heading>Acknowledgments</Heading><SimplePara>I thank Claude Kirchner for the many discussions on this paper.</SimplePara></ArticleNote></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>A Model-Based Completeness Proof of Extended Narrowing and Resolution</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>A Model-Based Completeness Proof of Extended Narrowing and Resolution</title></titleInfo><name type="personal"><namePart type="given">Jürgen</namePart><namePart type="family">Stuber</namePart><affiliation>INRIA LORIA, 615 Rue Jardin Botanique, 54600, Villers-les-Nancy, France</affiliation><affiliation>E-mail: stuber@loria.fr</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: We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.</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">1</identifier><part><date>2001</date><detail type="part"><title>A Model-Based Completeness Proof of Extended Narrowing and Resolution</title></detail><detail type="volume"><number>2083</number><caption>vol.</caption></detail><extent unit="pages"><start>195</start><end>210</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">F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36</identifier><identifier type="ark">ark:/67375/HCB-0496HD24-7</identifier><identifier type="DOI">10.1007/3-540-45744-5_15</identifier><identifier type="ChapterID">15</identifier><identifier type="ChapterID">Chap15</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-0496HD24-7/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 003966 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003966 | 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:F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36
|texte= A Model-Based Completeness Proof of Extended Narrowing and Resolution
}}
| This area was generated with Dilib version V0.6.33. |  |