Inductive proof search modulo
Identifieur interne : 001495 ( Istex/Corpus ); précédent : 001494; suivant : 001496Inductive proof search modulo
Auteurs : Fabrice Nahon ; Claude Kirchner ; Hélène Kirchner ; Paul BraunerSource :
- Annals of Mathematics and Artificial Intelligence [ 1012-2443 ] ; 2009-02-01.
English descriptors
Abstract
Abstract: We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.
Url:
DOI: 10.1007/s10472-009-9154-5
Links to Exploration step
ISTEX:5A358A18D109FE88ED19F481F5F7FD35D30429DBLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Inductive proof search modulo</title>
<author><name sortKey="Nahon, Fabrice" sort="Nahon, Fabrice" uniqKey="Nahon F" first="Fabrice" last="Nahon">Fabrice Nahon</name>
<affiliation><mods:affiliation>LORIA and Rectorat Nancy-Metz, Nancy-Metz, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Fabrice.Nahon@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation><mods:affiliation>INRIA, Bordeaux, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Claude.Kirchner@inria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name>
<affiliation><mods:affiliation>INRIA, Bordeaux, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Helene.Kirchner@inria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Brauner, Paul" sort="Brauner, Paul" uniqKey="Brauner P" first="Paul" last="Brauner">Paul Brauner</name>
<affiliation><mods:affiliation>LORIA and University of Nancy, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Paul.Brauner@loria.fr</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:5A358A18D109FE88ED19F481F5F7FD35D30429DB</idno>
<date when="2009" year="2009">2009</date>
<idno type="doi">10.1007/s10472-009-9154-5</idno>
<idno type="url">https://api.istex.fr/ark:/67375/VQC-FPHZD965-2/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001495</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001495</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Inductive proof search modulo</title>
<author><name sortKey="Nahon, Fabrice" sort="Nahon, Fabrice" uniqKey="Nahon F" first="Fabrice" last="Nahon">Fabrice Nahon</name>
<affiliation><mods:affiliation>LORIA and Rectorat Nancy-Metz, Nancy-Metz, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Fabrice.Nahon@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation><mods:affiliation>INRIA, Bordeaux, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Claude.Kirchner@inria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name>
<affiliation><mods:affiliation>INRIA, Bordeaux, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Helene.Kirchner@inria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Brauner, Paul" sort="Brauner, Paul" uniqKey="Brauner P" first="Paul" last="Brauner">Paul Brauner</name>
<affiliation><mods:affiliation>LORIA and University of Nancy, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: Paul.Brauner@loria.fr</mods:affiliation>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Annals of Mathematics and Artificial Intelligence</title>
<title level="j" type="abbrev">Ann Math Artif Intell</title>
<idno type="ISSN">1012-2443</idno>
<idno type="eISSN">1573-7470</idno>
<imprint><publisher>Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="2009-02-01">2009-02-01</date>
<biblScope unit="volume">55</biblScope>
<biblScope unit="issue">1-2</biblScope>
<biblScope unit="page" from="123">123</biblScope>
<biblScope unit="page" to="154">154</biblScope>
</imprint>
<idno type="ISSN">1012-2443</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">1012-2443</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Deduction modulo</term>
<term>Equational narrowing</term>
<term>Equational rewriting</term>
<term>Noetherian induction</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.</div>
</front>
</TEI>
<istex><corpusName>springer-journals</corpusName>
<author><json:item><name>Fabrice Nahon</name>
<affiliations><json:string>LORIA and Rectorat Nancy-Metz, Nancy-Metz, France</json:string>
<json:string>E-mail: Fabrice.Nahon@loria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Claude Kirchner</name>
<affiliations><json:string>INRIA, Bordeaux, France</json:string>
<json:string>E-mail: Claude.Kirchner@inria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Hélène Kirchner</name>
<affiliations><json:string>INRIA, Bordeaux, France</json:string>
<json:string>E-mail: Helene.Kirchner@inria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Paul Brauner</name>
<affiliations><json:string>LORIA and University of Nancy, Nancy, France</json:string>
<json:string>E-mail: Paul.Brauner@loria.fr</json:string>
</affiliations>
</json:item>
</author>
<subject><json:item><lang><json:string>eng</json:string>
</lang>
<value>Deduction modulo</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>Noetherian induction</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>Equational rewriting</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>Equational narrowing</value>
</json:item>
</subject>
<articleId><json:string>9154</json:string>
<json:string>s10472-009-9154-5</json:string>
</articleId>
<arkIstex>ark:/67375/VQC-FPHZD965-2</arkIstex>
<language><json:string>eng</json:string>
</language>
<originalGenre><json:string>OriginalPaper</json:string>
</originalGenre>
<abstract>Abstract: We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.</abstract>
<qualityIndicators><refBibsNative>false</refBibsNative>
<abstractWordCount>139</abstractWordCount>
<abstractCharCount>972</abstractCharCount>
<keywordCount>4</keywordCount>
<score>8.668</score>
<pdfWordCount>14763</pdfWordCount>
<pdfCharCount>67809</pdfCharCount>
<pdfVersion>1.3</pdfVersion>
<pdfPageCount>32</pdfPageCount>
<pdfPageSize>439.37 x 666.142 pts</pdfPageSize>
</qualityIndicators>
<title>Inductive proof search modulo</title>
<genre><json:string>research-article</json:string>
</genre>
<host><title>Annals of Mathematics and Artificial Intelligence</title>
<language><json:string>unknown</json:string>
</language>
<publicationDate>2009</publicationDate>
<copyrightDate>2009</copyrightDate>
<issn><json:string>1012-2443</json:string>
</issn>
<eissn><json:string>1573-7470</json:string>
</eissn>
<journalId><json:string>10472</json:string>
</journalId>
<volume>55</volume>
<issue>1-2</issue>
<pages><first>123</first>
<last>154</last>
</pages>
<genre><json:string>journal</json:string>
</genre>
<subject><json:item><value>Statistical Physics, Dynamical Systems and Complexity</value>
</json:item>
<json:item><value>Mathematics, general</value>
</json:item>
<json:item><value>Computer Science, general</value>
</json:item>
<json:item><value>Artificial Intelligence (incl. Robotics)</value>
</json:item>
</subject>
</host>
<ark><json:string>ark:/67375/VQC-FPHZD965-2</json:string>
</ark>
<publicationDate>2009</publicationDate>
<copyrightDate>2009</copyrightDate>
<doi><json:string>10.1007/s10472-009-9154-5</json:string>
</doi>
<id>5A358A18D109FE88ED19F481F5F7FD35D30429DB</id>
<score>1</score>
<fulltext><json:item><extension>pdf</extension>
<original>true</original>
<mimetype>application/pdf</mimetype>
<uri>https://api.istex.fr/ark:/67375/VQC-FPHZD965-2/fulltext.pdf</uri>
</json:item>
<json:item><extension>zip</extension>
<original>false</original>
<mimetype>application/zip</mimetype>
<uri>https://api.istex.fr/ark:/67375/VQC-FPHZD965-2/bundle.zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-FPHZD965-2/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Inductive proof search modulo</title>
</titleStmt>
<publicationStmt><authority>ISTEX</authority>
<publisher scheme="https://scientific-publisher.data.istex.fr">Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<availability><licence><p>Springer Science+Business Media B.V., 2009</p>
</licence>
<p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p>
</availability>
<date>2009</date>
</publicationStmt>
<notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note>
<note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note>
</notesStmt>
<sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Inductive proof search modulo</title>
<author xml:id="author-0000"><persName><forename type="first">Fabrice</forename>
<surname>Nahon</surname>
</persName>
<email>Fabrice.Nahon@loria.fr</email>
<affiliation>LORIA and Rectorat Nancy-Metz, Nancy-Metz, France</affiliation>
</author>
<author xml:id="author-0001" corresp="yes"><persName><forename type="first">Claude</forename>
<surname>Kirchner</surname>
</persName>
<email>Claude.Kirchner@inria.fr</email>
<affiliation>INRIA, Bordeaux, France</affiliation>
</author>
<author xml:id="author-0002"><persName><forename type="first">Hélène</forename>
<surname>Kirchner</surname>
</persName>
<email>Helene.Kirchner@inria.fr</email>
<affiliation>INRIA, Bordeaux, France</affiliation>
</author>
<author xml:id="author-0003"><persName><forename type="first">Paul</forename>
<surname>Brauner</surname>
</persName>
<email>Paul.Brauner@loria.fr</email>
<affiliation>LORIA and University of Nancy, Nancy, France</affiliation>
</author>
<idno type="istex">5A358A18D109FE88ED19F481F5F7FD35D30429DB</idno>
<idno type="ark">ark:/67375/VQC-FPHZD965-2</idno>
<idno type="DOI">10.1007/s10472-009-9154-5</idno>
<idno type="article-id">9154</idno>
<idno type="article-id">s10472-009-9154-5</idno>
</analytic>
<monogr><title level="j">Annals of Mathematics and Artificial Intelligence</title>
<title level="j" type="abbrev">Ann Math Artif Intell</title>
<idno type="pISSN">1012-2443</idno>
<idno type="eISSN">1573-7470</idno>
<idno type="journal-ID">true</idno>
<idno type="issue-article-count">7</idno>
<idno type="volume-issue-count">4</idno>
<imprint><publisher>Springer Netherlands</publisher>
<pubPlace>Dordrecht</pubPlace>
<date type="published" when="2009-02-01"></date>
<biblScope unit="volume">55</biblScope>
<biblScope unit="issue">1-2</biblScope>
<biblScope unit="page" from="123">123</biblScope>
<biblScope unit="page" to="154">154</biblScope>
</imprint>
</monogr>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><creation><date>2009</date>
</creation>
<langUsage><language ident="en">en</language>
</langUsage>
<abstract xml:lang="en"><p>Abstract: We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.</p>
</abstract>
<textClass xml:lang="en"><keywords scheme="keyword"><list><head>Keywords</head>
<item><term>Deduction modulo</term>
</item>
<item><term>Noetherian induction</term>
</item>
<item><term>Equational rewriting</term>
</item>
<item><term>Equational narrowing</term>
</item>
</list>
</keywords>
</textClass>
<textClass><classCode scheme="Mathematics Subject Classifications (2000)">68T15</classCode>
<classCode scheme="Mathematics Subject Classifications (2000)">03B35</classCode>
</textClass>
<textClass><keywords scheme="Journal Subject"><list><head>Computer Science</head>
<item><term>Statistical Physics, Dynamical Systems and Complexity</term>
</item>
<item><term>Mathematics, general</term>
</item>
<item><term>Computer Science, general</term>
</item>
<item><term>Artificial Intelligence (incl. Robotics)</term>
</item>
</list>
</keywords>
</textClass>
</profileDesc>
<revisionDesc><change when="2009-02-01">Published</change>
</revisionDesc>
</teiHeader>
</istex:fulltextTEI>
<json:item><extension>txt</extension>
<original>false</original>
<mimetype>text/plain</mimetype>
<uri>https://api.istex.fr/ark:/67375/VQC-FPHZD965-2/fulltext.txt</uri>
</json:item>
</fulltext>
<metadata><istex:metadataXml wicri:clean="corpus springer-journals 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 Netherlands</PublisherName>
<PublisherLocation>Dordrecht</PublisherLocation>
</PublisherInfo>
<Journal OutputMedium="All"><JournalInfo JournalProductType="NonStandardArchiveJournal" NumberingStyle="ContentOnly"><JournalID>10472</JournalID>
<JournalPrintISSN>1012-2443</JournalPrintISSN>
<JournalElectronicISSN>1573-7470</JournalElectronicISSN>
<JournalTitle>Annals of Mathematics and Artificial Intelligence</JournalTitle>
<JournalAbbreviatedTitle>Ann Math Artif Intell</JournalAbbreviatedTitle>
<JournalSubjectGroup><JournalSubject Type="Primary">Computer Science</JournalSubject>
<JournalSubject Type="Secondary">Statistical Physics, Dynamical Systems and Complexity</JournalSubject>
<JournalSubject Type="Secondary">Mathematics, general</JournalSubject>
<JournalSubject Type="Secondary">Computer Science, general</JournalSubject>
<JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject>
</JournalSubjectGroup>
</JournalInfo>
<Volume OutputMedium="All"><VolumeInfo TocLevels="0" VolumeType="Regular"><VolumeIDStart>55</VolumeIDStart>
<VolumeIDEnd>55</VolumeIDEnd>
<VolumeIssueCount>4</VolumeIssueCount>
</VolumeInfo>
<Issue IssueType="Combined" OutputMedium="All"><IssueInfo IssueType="Combined" TocLevels="0"><IssueIDStart>1</IssueIDStart>
<IssueIDEnd>2</IssueIDEnd>
<IssueTitle Language="En">Special Issue on First-Order Theorem Proving / Guest Edited by Silvio Ranise and Ullrich Hustadt</IssueTitle>
<IssueArticleCount>7</IssueArticleCount>
<IssueHistory><OnlineDate><Year>2009</Year>
<Month>10</Month>
<Day>6</Day>
</OnlineDate>
<PrintDate><Year>2009</Year>
<Month>10</Month>
<Day>5</Day>
</PrintDate>
<CoverDate><Year>2009</Year>
<Month>2</Month>
</CoverDate>
<PricelistYear>2009</PricelistYear>
</IssueHistory>
<IssueCopyright><CopyrightHolderName>Springer Science+Business Media B.V.</CopyrightHolderName>
<CopyrightYear>2009</CopyrightYear>
</IssueCopyright>
</IssueInfo>
<Article ID="s10472-009-9154-5" OutputMedium="All"><ArticleInfo ArticleType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="ContentOnly" TocLevels="0"><ArticleID>9154</ArticleID>
<ArticleDOI>10.1007/s10472-009-9154-5</ArticleDOI>
<ArticleCitationID>123</ArticleCitationID>
<ArticleSequenceNumber>6</ArticleSequenceNumber>
<ArticleTitle Language="En">Inductive proof search modulo</ArticleTitle>
<ArticleFirstPage>123</ArticleFirstPage>
<ArticleLastPage>154</ArticleLastPage>
<ArticleHistory><RegistrationDate><Year>2009</Year>
<Month>6</Month>
<Day>25</Day>
</RegistrationDate>
<OnlineDate><Year>2009</Year>
<Month>7</Month>
<Day>15</Day>
</OnlineDate>
</ArticleHistory>
<ArticleCopyright><CopyrightHolderName>Springer Science+Business Media B.V.</CopyrightHolderName>
<CopyrightYear>2009</CopyrightYear>
</ArticleCopyright>
<ArticleGrants 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>
</ArticleGrants>
</ArticleInfo>
<ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Fabrice</GivenName>
<FamilyName>Nahon</FamilyName>
</AuthorName>
<Contact><Email>Fabrice.Nahon@loria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff2" CorrespondingAffiliationID="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Claude</GivenName>
<FamilyName>Kirchner</FamilyName>
</AuthorName>
<Contact><Email>Claude.Kirchner@inria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Hélène</GivenName>
<FamilyName>Kirchner</FamilyName>
</AuthorName>
<Contact><Email>Helene.Kirchner@inria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff3"><AuthorName DisplayOrder="Western"><GivenName>Paul</GivenName>
<FamilyName>Brauner</FamilyName>
</AuthorName>
<Contact><Email>Paul.Brauner@loria.fr</Email>
</Contact>
</Author>
<Affiliation ID="Aff1"><OrgName>LORIA and Rectorat Nancy-Metz</OrgName>
<OrgAddress><City>Nancy-Metz</City>
<Country Code="FR">France</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff2"><OrgName>INRIA</OrgName>
<OrgAddress><City>Bordeaux</City>
<Country Code="FR">France</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff3"><OrgName>LORIA and University of Nancy</OrgName>
<OrgAddress><City>Nancy</City>
<Country Code="FR">France</Country>
</OrgAddress>
</Affiliation>
</AuthorGroup>
<Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading>
<Para TextBreak="No">We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system <InlineEquation ID="IEq1"><InlineMediaObject><ImageObject Color="BlackWhite" FileRef="10472_2009_9154_Article_IEq1.gif" Format="GIF" Rendition="HTML" Type="Linedraw"></ImageObject>
</InlineMediaObject>
<EquationSource Format="TEX">$\mathcal{R}$</EquationSource>
</InlineEquation>
and a set <Emphasis Type="Italic">E</Emphasis>
of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system <InlineEquation ID="IEq2"><InlineMediaObject><ImageObject Color="BlackWhite" FileRef="10472_2009_9154_Article_IEq2.gif" Format="GIF" Rendition="HTML" Type="Linedraw"></ImageObject>
</InlineMediaObject>
<EquationSource Format="TEX">$(\mathcal{R},E)$</EquationSource>
</InlineEquation>
has good properties of termination, sufficient completeness, and when <Emphasis Type="Italic">E</Emphasis>
is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.</Para>
</Abstract>
<KeywordGroup Language="En"><Heading>Keywords</Heading>
<Keyword>Deduction modulo</Keyword>
<Keyword>Noetherian induction</Keyword>
<Keyword>Equational rewriting</Keyword>
<Keyword>Equational narrowing</Keyword>
</KeywordGroup>
<KeywordGroup Language="--"><Heading>Mathematics Subject Classifications (2000)</Heading>
<Keyword>68T15</Keyword>
<Keyword>03B35</Keyword>
</KeywordGroup>
</ArticleHeader>
<NoBody></NoBody>
</Article>
</Issue>
</Volume>
</Journal>
</Publisher>
</istex:document>
</istex:metadataXml>
<mods version="3.6"><titleInfo lang="en"><title>Inductive proof search modulo</title>
</titleInfo>
<titleInfo type="alternative" contentType="CDATA"><title>Inductive proof search modulo</title>
</titleInfo>
<name type="personal"><namePart type="given">Fabrice</namePart>
<namePart type="family">Nahon</namePart>
<affiliation>LORIA and Rectorat Nancy-Metz, Nancy-Metz, France</affiliation>
<affiliation>E-mail: Fabrice.Nahon@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal" displayLabel="corresp"><namePart type="given">Claude</namePart>
<namePart type="family">Kirchner</namePart>
<affiliation>INRIA, Bordeaux, France</affiliation>
<affiliation>E-mail: Claude.Kirchner@inria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Hélène</namePart>
<namePart type="family">Kirchner</namePart>
<affiliation>INRIA, Bordeaux, France</affiliation>
<affiliation>E-mail: Helene.Kirchner@inria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Paul</namePart>
<namePart type="family">Brauner</namePart>
<affiliation>LORIA and University of Nancy, Nancy, France</affiliation>
<affiliation>E-mail: Paul.Brauner@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<typeOfResource>text</typeOfResource>
<genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre>
<originInfo><publisher>Springer Netherlands</publisher>
<place><placeTerm type="text">Dordrecht</placeTerm>
</place>
<dateIssued encoding="w3cdtf">2009-02-01</dateIssued>
<copyrightDate encoding="w3cdtf">2009</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="rfc3066">en</languageTerm>
<languageTerm type="code" authority="iso639-2b">eng</languageTerm>
</language>
<abstract lang="en">Abstract: We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.</abstract>
<subject lang="en"><genre>Keywords</genre>
<topic>Deduction modulo</topic>
<topic>Noetherian induction</topic>
<topic>Equational rewriting</topic>
<topic>Equational narrowing</topic>
</subject>
<classification displayLabel="Mathematics Subject Classifications (2000)">68T15</classification>
<classification displayLabel="Mathematics Subject Classifications (2000)">03B35</classification>
<relatedItem type="host"><titleInfo><title>Annals of Mathematics and Artificial Intelligence</title>
</titleInfo>
<titleInfo type="abbreviated"><title>Ann Math Artif Intell</title>
</titleInfo>
<genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre>
<originInfo><publisher>Springer</publisher>
<dateIssued encoding="w3cdtf">2009-10-06</dateIssued>
<copyrightDate encoding="w3cdtf">2009</copyrightDate>
</originInfo>
<subject><genre>Computer Science</genre>
<topic>Statistical Physics, Dynamical Systems and Complexity</topic>
<topic>Mathematics, general</topic>
<topic>Computer Science, general</topic>
<topic>Artificial Intelligence (incl. Robotics)</topic>
</subject>
<identifier type="ISSN">1012-2443</identifier>
<identifier type="eISSN">1573-7470</identifier>
<identifier type="JournalID">10472</identifier>
<identifier type="IssueArticleCount">7</identifier>
<identifier type="VolumeIssueCount">4</identifier>
<part><date>2009</date>
<detail type="issue"><title>Special Issue on First-Order Theorem Proving / Guest Edited by Silvio Ranise and Ullrich Hustadt</title>
</detail>
<detail type="volume"><number>55</number>
<caption>vol.</caption>
</detail>
<detail type="issue"><number>1-2</number>
<caption>no.</caption>
</detail>
<extent unit="pages"><start>123</start>
<end>154</end>
</extent>
</part>
<recordInfo><recordOrigin>Springer Science+Business Media B.V., 2009</recordOrigin>
</recordInfo>
</relatedItem>
<identifier type="istex">5A358A18D109FE88ED19F481F5F7FD35D30429DB</identifier>
<identifier type="ark">ark:/67375/VQC-FPHZD965-2</identifier>
<identifier type="DOI">10.1007/s10472-009-9154-5</identifier>
<identifier type="ArticleID">9154</identifier>
<identifier type="ArticleID">s10472-009-9154-5</identifier>
<accessCondition type="use and reproduction" contentType="copyright">Springer Science+Business Media B.V., 2009</accessCondition>
<recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource>
<recordOrigin>Springer Science+Business Media B.V., 2009</recordOrigin>
</recordInfo>
</mods>
<json:item><extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/ark:/67375/VQC-FPHZD965-2/record.json</uri>
</json:item>
</metadata>
<serie></serie>
</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 001495 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001495 | 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:5A358A18D109FE88ED19F481F5F7FD35D30429DB |texte= Inductive proof search modulo }}
This area was generated with Dilib version V0.6.33. |