Associative-commutative deduction with constraints
Identifieur interne : 000C28 ( Istex/Corpus ); précédent : 000C27; suivant : 000C29Associative-commutative deduction with constraints
Auteurs : Laurent VigneronSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.
Url:
DOI: 10.1007/3-540-58156-1_39
Links to Exploration step
ISTEX:33D94BA77B14357C4B323398C1C10B05541C9E41Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Associative-commutative deduction with constraints</title><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation><mods:affiliation>CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: laurent.vigneron@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:33D94BA77B14357C4B323398C1C10B05541C9E41</idno><date when="1994" year="1994">1994</date><idno type="doi">10.1007/3-540-58156-1_39</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-LRK8CXQ3-W/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000C28</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000C28</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Associative-commutative deduction with constraints</title><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation><mods:affiliation>CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: laurent.vigneron@loria.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</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: Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Laurent Vigneron</name><affiliations><json:string>CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France</json:string><json:string>E-mail: laurent.vigneron@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-LRK8CXQ3-W</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>ReviewPaper</json:string></originalGenre><abstract>Abstract: Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.</abstract><qualityIndicators><score>8.416</score><pdfWordCount>9185</pdfWordCount><pdfCharCount>42463</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>439.2 x 666 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>118</abstractWordCount><abstractCharCount>783</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Associative-commutative deduction with constraints</title><chapterId><json:string>39</json:string><json:string>Chap39</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>1994</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>J. G. Carbonell</name></json:item><json:item><name>J. Siekmann</name></json:item><json:item><name>G. Goos</name></json:item><json:item><name>J. Hartmanis</name></json:item></editor></serie><host><title>Automated Deduction — CADE-12</title><language><json:string>unknown</json:string></language><copyrightDate>1994</copyrightDate><doi><json:string>10.1007/3-540-58156-1</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-48467-7</json:string></eisbn><bookId><json:string>3540581561</json:string></bookId><isbn><json:string>978-3-540-58156-7</json:string></isbn><volume>814</volume><pages><first>530</first><last>544</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Alan Bundy</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>Mathematical Logic and Foundations</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-LRK8CXQ3-W</json:string></ark><publicationDate>1994</publicationDate><copyrightDate>1994</copyrightDate><doi><json:string>10.1007/3-540-58156-1_39</json:string></doi><id>33D94BA77B14357C4B323398C1C10B05541C9E41</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-LRK8CXQ3-W/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-LRK8CXQ3-W/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-LRK8CXQ3-W/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Associative-commutative deduction with constraints</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag</licence></availability><date when="1994">1994</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">Associative-commutative deduction with constraints</title><author><persName><forename type="first">Laurent</forename><surname>Vigneron</surname></persName><email>laurent.vigneron@loria.fr</email><affiliation><orgName type="institution">CRIN-CNRS & INRIA-Lorraine</orgName><address><postBox>BP 239</postBox><postCode>54506</postCode><settlement>Vandœuvre-lès-Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">33D94BA77B14357C4B323398C1C10B05541C9E41</idno><idno type="ark">ark:/67375/HCB-LRK8CXQ3-W</idno><idno type="DOI">10.1007/3-540-58156-1_39</idno></analytic><monogr><title level="m" type="main">Automated Deduction — CADE-12</title><title level="m" type="sub">12th International Conference on Automated Deduction Nancy, France, June 26 – July 1, 1994 Proceedings</title><idno type="DOI">10.1007/3-540-58156-1</idno><idno type="book-id">3540581561</idno><idno type="ISBN">978-3-540-58156-7</idno><idno type="eISBN">978-3-540-48467-7</idno><idno type="chapter-id">Chap39</idno><editor><persName><forename type="first">Alan</forename><surname>Bundy</surname></persName></editor><imprint><biblScope unit="vol">814</biblScope><biblScope unit="page" from="530">530</biblScope><biblScope unit="page" to="544">544</biblScope><biblScope unit="chapter-count">72</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><editor><persName><forename type="first">J.</forename><forename type="first">G.</forename><surname>Carbonell</surname></persName></editor><editor><persName><forename type="first">J.</forename><surname>Siekmann</surname></persName></editor><editor><persName><forename type="first">G.</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><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>Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.</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>M24005</label><item><term type="Secondary" subtype="priority-3">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-LRK8CXQ3-W/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 TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle><SeriesSubTitle Language="En">Lecture Notes in Artificial Intelligence (LNAI)</SeriesSubTitle><SeriesAbbreviatedTitle>Lect Notes Comput Sci</SeriesAbbreviatedTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo MediaType="eBook" Language="En" BookProductType="Proceedings" TocLevels="0" NumberingStyle="Unnumbered"><BookID>3540581561</BookID><BookTitle>Automated Deduction — CADE-12</BookTitle><BookSubTitle>12th International Conference on Automated Deduction Nancy, France, June 26 – July 1, 1994 Proceedings</BookSubTitle><BookVolumeNumber>814</BookVolumeNumber><BookDOI>10.1007/3-540-58156-1</BookDOI><BookTitleID>39035</BookTitleID><BookPrintISBN>978-3-540-58156-7</BookPrintISBN><BookElectronicISBN>978-3-540-48467-7</BookElectronicISBN><BookChapterCount>72</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1994</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="M24005" Priority="3" Type="Secondary">Mathematical Logic and Foundations</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Alan</GivenName><FamilyName>Bundy</FamilyName></EditorName></Editor></EditorGroup></BookHeader><Chapter ID="Chap39" Language="En"><ChapterInfo ChapterType="ReviewPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ChapterID>39</ChapterID><ChapterDOI>10.1007/3-540-58156-1_39</ChapterDOI><ChapterSequenceNumber>39</ChapterSequenceNumber><ChapterTitle Language="En">Associative-commutative deduction with constraints</ChapterTitle><ChapterFirstPage>530</ChapterFirstPage><ChapterLastPage>544</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1994</CopyrightYear></ChapterCopyright><ChapterHistory><OnlineDate><Year>2005</Year><Month>5</Month><Day>30</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><BookID>3540581561</BookID><BookTitle>Automated Deduction — CADE-12</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Laurent</GivenName><FamilyName>Vigneron</FamilyName></AuthorName><Contact><Email>laurent.vigneron@loria.fr</Email></Contact></Author><Affiliation ID="Aff1"><OrgName>CRIN-CNRS & INRIA-Lorraine</OrgName><OrgAddress><Postbox>BP 239</Postbox><Postcode>54506</Postcode><City>Vandœuvre-lès-Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>This work is partially supported by the GDR Programmation and the Esprit Basic Research working group 6028, CCL.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Associative-commutative deduction with constraints</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Associative-commutative deduction with constraints</title></titleInfo><name type="personal"><namePart type="given">Laurent</namePart><namePart type="family">Vigneron</namePart><affiliation>CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: laurent.vigneron@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="ReviewPaper" 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">1994</dateIssued><copyrightDate encoding="w3cdtf">1994</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: Associative-commutative equational reasoning is known to be highly complex for theorem proving. Hence, it is very important to focus deduction by adding constraints, such as unification and ordering, and to define efficient strategies, such as the basic requirements à la Hullot. Constraints are formulas used for pruning the set of ground instances of clauses deduced by a theorem prover. We propose here an extension of AC-paramodulation and AC-superposition with these constraint mechanisms; we do not need to compute AC-unifiers anymore. The method is proved to be refutationally complete, even with simplification. The power of this approach is exemplified by a very short proof of the equational version of SAM's Lemma using DATAC, our implementation of the strategy.</abstract><relatedItem type="host"><titleInfo><title>Automated Deduction — CADE-12</title><subTitle>12th International Conference on Automated Deduction Nancy, France, June 26 – July 1, 1994 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Alan</namePart><namePart type="family">Bundy</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">1994</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="M24005">Mathematical Logic and Foundations</topic></subject><identifier type="DOI">10.1007/3-540-58156-1</identifier><identifier type="ISBN">978-3-540-58156-7</identifier><identifier type="eISBN">978-3-540-48467-7</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">39035</identifier><identifier type="BookID">3540581561</identifier><identifier type="BookChapterCount">72</identifier><identifier type="BookVolumeNumber">814</identifier><part><date>1994</date><detail type="volume"><number>814</number><caption>vol.</caption></detail><extent unit="pages"><start>530</start><end>544</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 1994</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title><subTitle>Lecture Notes in Artificial Intelligence (LNAI)</subTitle></titleInfo><name type="personal"><namePart type="given">J.</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.</namePart><namePart type="family">Siekmann</namePart><role><roleTerm type="text">editor</roleTerm></role></name><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><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1994</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag, 1994</recordOrigin></recordInfo></relatedItem><identifier type="istex">33D94BA77B14357C4B323398C1C10B05541C9E41</identifier><identifier type="ark">ark:/67375/HCB-LRK8CXQ3-W</identifier><identifier type="DOI">10.1007/3-540-58156-1_39</identifier><identifier type="ChapterID">39</identifier><identifier type="ChapterID">Chap39</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 1994</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, 1994</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-LRK8CXQ3-W/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 000C28 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000C28 | 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:33D94BA77B14357C4B323398C1C10B05541C9E41
|texte= Associative-commutative deduction with constraints
}}
| This area was generated with Dilib version V0.6.33. |  |