Automatic Decidability and Combinability Revisited
Identifieur interne : 002F73 ( Istex/Corpus ); précédent : 002F72; suivant : 002F74Automatic Decidability and Combinability Revisited
Auteurs : Christopher Lynch ; Duc-Khanh TranSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We present an inference system for clauses with ordering constraints, called Schematic Paramodulation. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality X = Y then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska’s meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska’s meta-saturation does not halt.
Url:
DOI: 10.1007/978-3-540-73595-3_22
Links to Exploration step
ISTEX:C92807B3EB586D6054143FA0A4A627B440CFB013Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automatic Decidability and Combinability Revisited</title><author><name sortKey="Lynch, Christopher" sort="Lynch, Christopher" uniqKey="Lynch C" first="Christopher" last="Lynch">Christopher Lynch</name><affiliation><mods:affiliation>Clarkson University, USA</mods:affiliation></affiliation></author><author><name sortKey="Tran, Duc Khanh" sort="Tran, Duc Khanh" uniqKey="Tran D" first="Duc-Khanh" last="Tran">Duc-Khanh Tran</name><affiliation><mods:affiliation>LORIA & INRIA-Lorraine, France</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:C92807B3EB586D6054143FA0A4A627B440CFB013</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/978-3-540-73595-3_22</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-2F5470VT-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002F73</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002F73</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automatic Decidability and Combinability Revisited</title><author><name sortKey="Lynch, Christopher" sort="Lynch, Christopher" uniqKey="Lynch C" first="Christopher" last="Lynch">Christopher Lynch</name><affiliation><mods:affiliation>Clarkson University, USA</mods:affiliation></affiliation></author><author><name sortKey="Tran, Duc Khanh" sort="Tran, Duc Khanh" uniqKey="Tran D" first="Duc-Khanh" last="Tran">Duc-Khanh Tran</name><affiliation><mods:affiliation>LORIA & INRIA-Lorraine, France</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="eISSN">1611-3349</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 present an inference system for clauses with ordering constraints, called Schematic Paramodulation. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality X = Y then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska’s meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska’s meta-saturation does not halt.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Christopher Lynch</name><affiliations><json:string>Clarkson University, USA</json:string></affiliations></json:item><json:item><name>Duc-Khanh Tran</name><affiliations><json:string>LORIA & INRIA-Lorraine, France</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-2F5470VT-P</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We present an inference system for clauses with ordering constraints, called Schematic Paramodulation. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality X = Y then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska’s meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska’s meta-saturation does not halt.</abstract><qualityIndicators><score>8.68</score><pdfWordCount>7801</pdfWordCount><pdfCharCount>35682</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>17</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>140</abstractWordCount><abstractCharCount>1042</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Automatic Decidability and Combinability Revisited</title><chapterId><json:string>22</json:string><json:string>Chap22</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>2007</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn></serie><host><title>Automated Deduction – CADE-21</title><language><json:string>unknown</json:string></language><copyrightDate>2007</copyrightDate><doi><json:string>10.1007/978-3-540-73595-3</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-73595-3</json:string></eisbn><bookId><json:string>978-3-540-73595-3</json:string></bookId><isbn><json:string>978-3-540-73594-6</json:string></isbn><volume>4603</volume><pages><first>328</first><last>344</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Frank Pfenning</name></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></subject></host><ark><json:string>ark:/67375/HCB-2F5470VT-P</json:string></ark><publicationDate>2007</publicationDate><copyrightDate>2007</copyrightDate><doi><json:string>10.1007/978-3-540-73595-3_22</json:string></doi><id>C92807B3EB586D6054143FA0A4A627B440CFB013</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-2F5470VT-P/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-2F5470VT-P/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-2F5470VT-P/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Automatic Decidability and Combinability Revisited</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2007">2007</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">Automatic Decidability and Combinability Revisited</title><author><persName><forename type="first">Christopher</forename><surname>Lynch</surname></persName><affiliation><orgName type="institution">Clarkson University</orgName><address><country key="US">UNITED STATES</country></address></affiliation></author><author><persName><forename type="first">Duc-Khanh</forename><surname>Tran</surname></persName><affiliation><orgName type="institution">LORIA & INRIA-Lorraine</orgName><address><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">C92807B3EB586D6054143FA0A4A627B440CFB013</idno><idno type="ark">ark:/67375/HCB-2F5470VT-P</idno><idno type="DOI">10.1007/978-3-540-73595-3_22</idno></analytic><monogr><title level="m" type="main">Automated Deduction – CADE-21</title><title level="m" type="sub">21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings</title><title level="m" type="part">Session 8. First-Order Logic</title><idno type="DOI">10.1007/978-3-540-73595-3</idno><idno type="book-id">978-3-540-73595-3</idno><idno type="ISBN">978-3-540-73594-6</idno><idno type="eISBN">978-3-540-73595-3</idno><idno type="chapter-id">Chap22</idno><idno type="part-id">Part8</idno><editor><persName><forename type="first">Frank</forename><surname>Pfenning</surname></persName><email>fp@cs.cmu.edu</email></editor><imprint><biblScope unit="vol">4603</biblScope><biblScope unit="page" from="328">328</biblScope><biblScope unit="page" to="344">344</biblScope><biblScope unit="chapter-count">38</biblScope><biblScope unit="part-chapter-count">4</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>We present an inference system for clauses with ordering constraints, called <hi rend="italic">Schematic Paramodulation</hi>. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality <hi rend="italic">X</hi> = <hi rend="italic">Y</hi> then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska’s meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska’s meta-saturation does not halt.</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></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-2F5470VT-P/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><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN><SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor></EditorGroup></SubSeriesHeader></SubSeries><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" OutputMedium="All" TocLevels="0"><BookID>978-3-540-73595-3</BookID><BookTitle>Automated Deduction – CADE-21</BookTitle><BookSubTitle>21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings</BookSubTitle><BookVolumeNumber>4603</BookVolumeNumber><BookSequenceNumber>4603</BookSequenceNumber><BookDOI>10.1007/978-3-540-73595-3</BookDOI><BookTitleID>151090</BookTitleID><BookPrintISBN>978-3-540-73594-6</BookPrintISBN><BookElectronicISBN>978-3-540-73595-3</BookElectronicISBN><BookChapterCount>38</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2007</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><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Frank</GivenName><FamilyName>Pfenning</FamilyName></EditorName><Contact><Email>fp@cs.cmu.edu</Email></Contact></Editor></EditorGroup></BookHeader><Part ID="Part8"><PartInfo TocLevels="0"><PartID>8</PartID><PartSequenceNumber>8</PartSequenceNumber><PartTitle>Session 8. First-Order Logic</PartTitle><PartChapterCount>4</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Automated Deduction – CADE-21</BookTitle></PartContext></PartInfo><Chapter ID="Chap22" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>22</ChapterID><ChapterDOI>10.1007/978-3-540-73595-3_22</ChapterDOI><ChapterSequenceNumber>22</ChapterSequenceNumber><ChapterTitle Language="En">Automatic Decidability and Combinability Revisited</ChapterTitle><ChapterFirstPage>328</ChapterFirstPage><ChapterLastPage>344</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></ChapterCopyright><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>8</PartID><BookID>978-3-540-73595-3</BookID><BookTitle>Automated Deduction – CADE-21</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Christopher</GivenName><FamilyName>Lynch</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Duc-Khanh</GivenName><FamilyName>Tran</FamilyName></AuthorName></Author><Affiliation ID="Aff1"><OrgName>Clarkson University</OrgName><OrgAddress><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>LORIA & INRIA-Lorraine</OrgName><OrgAddress><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We present an inference system for clauses with ordering constraints, called <Emphasis Type="Italic">Schematic Paramodulation</Emphasis>. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality <Emphasis Type="Italic">X</Emphasis> = <Emphasis Type="Italic">Y</Emphasis> then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska’s meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska’s meta-saturation does not halt.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Automatic Decidability and Combinability Revisited</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Automatic Decidability and Combinability Revisited</title></titleInfo><name type="personal"><namePart type="given">Christopher</namePart><namePart type="family">Lynch</namePart><affiliation>Clarkson University, USA</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Duc-Khanh</namePart><namePart type="family">Tran</namePart><affiliation>LORIA & INRIA-Lorraine, France</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">2007</dateIssued><copyrightDate encoding="w3cdtf">2007</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 inference system for clauses with ordering constraints, called Schematic Paramodulation. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality X = Y then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska’s meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska’s meta-saturation does not halt.</abstract><relatedItem type="host"><titleInfo><title>Automated Deduction – CADE-21</title><subTitle>21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Frank</namePart><namePart type="family">Pfenning</namePart><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">2007</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></subject><identifier type="DOI">10.1007/978-3-540-73595-3</identifier><identifier type="ISBN">978-3-540-73594-6</identifier><identifier type="eISBN">978-3-540-73595-3</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">151090</identifier><identifier type="BookID">978-3-540-73595-3</identifier><identifier type="BookChapterCount">38</identifier><identifier type="BookVolumeNumber">4603</identifier><identifier type="BookSequenceNumber">4603</identifier><identifier type="PartChapterCount">4</identifier><part><date>2007</date><detail type="part"><title>Session 8. First-Order Logic</title></detail><detail type="volume"><number>4603</number><caption>vol.</caption></detail><extent unit="pages"><start>328</start><end>344</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2007</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2007</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Frank</namePart><namePart type="family">Pfenning</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2007</recordOrigin></recordInfo></relatedItem><identifier type="istex">C92807B3EB586D6054143FA0A4A627B440CFB013</identifier><identifier type="ark">ark:/67375/HCB-2F5470VT-P</identifier><identifier type="DOI">10.1007/978-3-540-73595-3_22</identifier><identifier type="ChapterID">22</identifier><identifier type="ChapterID">Chap22</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2007</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, 2007</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-2F5470VT-P/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 002F73 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002F73 | 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:C92807B3EB586D6054143FA0A4A627B440CFB013
|texte= Automatic Decidability and Combinability Revisited
}}
| This area was generated with Dilib version V0.6.33. |  |