Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Inductive proof search modulo

Identifieur interne : 001495 ( Istex/Corpus ); précédent : 001494; suivant : 001496

Inductive proof search modulo

Auteurs : Fabrice Nahon ; Claude Kirchner ; Hélène Kirchner ; Paul Brauner

Source :

RBID : ISTEX:5A358A18D109FE88ED19F481F5F7FD35D30429DB

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:5A358A18D109FE88ED19F481F5F7FD35D30429DB

Le 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
}}

Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022