Linear logic with isabelle: Pruning the proof search tree
Identifieur interne : 002199 ( Istex/Corpus ); précédent : 002198; suivant : 002200Linear logic with isabelle: Pruning the proof search tree
Auteurs : Philippe De GrooteSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.
Url:
DOI: 10.1007/3-540-59338-1_41
Links to Exploration step
ISTEX:91F30B6F2190128B051C37FC2C7CEA0C0DA04F16Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Linear logic with isabelle: Pruning the proof search tree</title><author><name sortKey="De Groote, Philippe" sort="De Groote, Philippe" uniqKey="De Groote P" first="Philippe" last="De Groote">Philippe De Groote</name><affiliation><mods:affiliation>INRIA-Lorraine-CRIN-CNRS, 615 rue du Jardin Botanique, B.P. 101, F 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Philippe.de.Groote@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:91F30B6F2190128B051C37FC2C7CEA0C0DA04F16</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1007/3-540-59338-1_41</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-Z30MZMQ9-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002199</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002199</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Linear logic with isabelle: Pruning the proof search tree</title><author><name sortKey="De Groote, Philippe" sort="De Groote, Philippe" uniqKey="De Groote P" first="Philippe" last="De Groote">Philippe De Groote</name><affiliation><mods:affiliation>INRIA-Lorraine-CRIN-CNRS, 615 rue du Jardin Botanique, B.P. 101, F 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Philippe.de.Groote@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: This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Philippe de Groote</name><affiliations><json:string>INRIA-Lorraine-CRIN-CNRS, 615 rue du Jardin Botanique, B.P. 101, F 54602, Villers-lès-Nancy Cedex, France</json:string><json:string>E-mail: Philippe.de.Groote@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-Z30MZMQ9-H</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>ReviewPaper</json:string></originalGenre><abstract>Abstract: This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.</abstract><qualityIndicators><score>7.493</score><pdfWordCount>4845</pdfWordCount><pdfCharCount>23597</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>439.28 x 666 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>54</abstractWordCount><abstractCharCount>377</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Linear logic with isabelle: Pruning the proof search tree</title><chapterId><json:string>18</json:string><json:string>Chap18</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>1995</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>G. Goos</name></json:item><json:item><name>J. Hartmanis</name></json:item><json:item><name>J. van Leeuwen</name></json:item><json:item><name>Jaime G. Carbonell</name></json:item><json:item><name>Jörg Siekmann</name></json:item></editor></serie><host><title>Theorem Proving with Analytic Tableaux and Related Methods</title><language><json:string>unknown</json:string></language><copyrightDate>1995</copyrightDate><doi><json:string>10.1007/3-540-59338-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-49235-1</json:string></eisbn><bookId><json:string>3540593381</json:string></bookId><isbn><json:string>978-3-540-59338-6</json:string></isbn><volume>918</volume><pages><first>263</first><last>277</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Peter Baumgartner</name></json:item><json:item><name>Reiner Hähnle</name></json:item><json:item><name>Joachim Possega</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-Z30MZMQ9-H</json:string></ark><publicationDate>1995</publicationDate><copyrightDate>1995</copyrightDate><doi><json:string>10.1007/3-540-59338-1_41</json:string></doi><id>91F30B6F2190128B051C37FC2C7CEA0C0DA04F16</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-Z30MZMQ9-H/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-Z30MZMQ9-H/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-Z30MZMQ9-H/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Linear logic with isabelle: Pruning the proof search tree</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag</licence></availability><date when="1995">1995</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">Linear logic with isabelle: Pruning the proof search tree</title><author><persName><forename type="first">Philippe</forename><nameLink>de</nameLink><surname>Groote</surname></persName><email>Philippe.de.Groote@loria.fr</email><affiliation><orgName type="institution">INRIA-Lorraine-CRIN-CNRS</orgName><address><street>615 rue du Jardin Botanique</street><postBox>B.P. 101</postBox><postCode>F 54602</postCode><settlement>Villers-lès-Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">91F30B6F2190128B051C37FC2C7CEA0C0DA04F16</idno><idno type="ark">ark:/67375/HCB-Z30MZMQ9-H</idno><idno type="DOI">10.1007/3-540-59338-1_41</idno></analytic><monogr><title level="m" type="main">Theorem Proving with Analytic Tableaux and Related Methods</title><title level="m" type="sub">4th International Workshop, TABLEAUX '95 Schloß Reinfels, St. Goar, Germany, May 7–10, 1995 Proceedings</title><idno type="DOI">10.1007/3-540-59338-1</idno><idno type="book-id">3540593381</idno><idno type="ISBN">978-3-540-59338-6</idno><idno type="eISBN">978-3-540-49235-1</idno><idno type="chapter-id">Chap18</idno><editor><persName><forename type="first">Peter</forename><surname>Baumgartner</surname></persName></editor><editor><persName><forename type="first">Reiner</forename><surname>Hähnle</surname></persName></editor><editor><persName><forename type="first">Joachim</forename><surname>Possega</surname></persName></editor><imprint><biblScope unit="vol">918</biblScope><biblScope unit="page" from="263">263</biblScope><biblScope unit="page" to="277">277</biblScope><biblScope unit="chapter-count">23</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">G.</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><editor><persName><forename type="first">J.</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName></editor><editor><persName><forename type="first">Jaime</forename><forename type="first">G.</forename><surname>Carbonell</surname></persName></editor><editor><persName><forename type="first">Jörg</forename><surname>Siekmann</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>This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.</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-Z30MZMQ9-H/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</SeriesSubTitle><SeriesAbbreviatedTitle>Lect Notes Comput Sci</SeriesAbbreviatedTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><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></SeriesHeader><Book Language="En"><BookInfo MediaType="eBook" Language="En" BookProductType="Proceedings" TocLevels="0" NumberingStyle="Unnumbered"><BookID>3540593381</BookID><BookTitle>Theorem Proving with Analytic Tableaux and Related Methods</BookTitle><BookSubTitle>4th International Workshop, TABLEAUX '95 Schloß Reinfels, St. Goar, Germany, May 7–10, 1995 Proceedings</BookSubTitle><BookVolumeNumber>918</BookVolumeNumber><BookDOI>10.1007/3-540-59338-1</BookDOI><BookTitleID>42682</BookTitleID><BookPrintISBN>978-3-540-59338-6</BookPrintISBN><BookElectronicISBN>978-3-540-49235-1</BookElectronicISBN><BookChapterCount>23</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1995</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>Peter</GivenName><FamilyName>Baumgartner</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Reiner</GivenName><FamilyName>Hähnle</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Joachim</GivenName><FamilyName>Possega</FamilyName></EditorName></Editor></EditorGroup></BookHeader><Chapter ID="Chap18" Language="En"><ChapterInfo ChapterType="ReviewPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ChapterID>18</ChapterID><ChapterDOI>10.1007/3-540-59338-1_41</ChapterDOI><ChapterSequenceNumber>18</ChapterSequenceNumber><ChapterTitle Language="En">Linear logic with isabelle: Pruning the proof search tree</ChapterTitle><ChapterCategory>Linear Logic</ChapterCategory><ChapterFirstPage>263</ChapterFirstPage><ChapterLastPage>277</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1995</CopyrightYear></ChapterCopyright><ChapterHistory><OnlineDate><Year>2005</Year><Month>6</Month><Day>2</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>3540593381</BookID><BookTitle>Theorem Proving with Analytic Tableaux and Related Methods</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Philippe</GivenName><Particle>de</Particle><FamilyName>Groote</FamilyName></AuthorName><Contact><Email>Philippe.de.Groote@loria.fr</Email></Contact></Author><Affiliation ID="Aff1"><OrgName>INRIA-Lorraine-CRIN-CNRS</OrgName><OrgAddress><Street>615 rue du Jardin Botanique</Street><Postbox>B.P. 101</Postbox><Postcode>F 54602</Postcode><City>Villers-lès-Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Linear logic with isabelle: Pruning the proof search tree</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Linear logic with isabelle: Pruning the proof search tree</title></titleInfo><name type="personal"><namePart type="given">Philippe</namePart><namePart type="family">de Groote</namePart><affiliation>INRIA-Lorraine-CRIN-CNRS, 615 rue du Jardin Botanique, B.P. 101, F 54602, Villers-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: Philippe.de.Groote@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">1995</dateIssued><copyrightDate encoding="w3cdtf">1995</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.</abstract><relatedItem type="host"><titleInfo><title>Theorem Proving with Analytic Tableaux and Related Methods</title><subTitle>4th International Workshop, TABLEAUX '95 Schloß Reinfels, St. Goar, Germany, May 7–10, 1995 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Peter</namePart><namePart type="family">Baumgartner</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Reiner</namePart><namePart type="family">Hähnle</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Joachim</namePart><namePart type="family">Possega</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">1995</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-59338-1</identifier><identifier type="ISBN">978-3-540-59338-6</identifier><identifier type="eISBN">978-3-540-49235-1</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">42682</identifier><identifier type="BookID">3540593381</identifier><identifier type="BookChapterCount">23</identifier><identifier type="BookVolumeNumber">918</identifier><part><date>1995</date><detail type="volume"><number>918</number><caption>vol.</caption></detail><extent unit="pages"><start>263</start><end>277</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 1995</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title><subTitle>Lecture Notes in Artificial Intelligence</subTitle></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">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><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1995</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, 1995</recordOrigin></recordInfo></relatedItem><identifier type="istex">91F30B6F2190128B051C37FC2C7CEA0C0DA04F16</identifier><identifier type="ark">ark:/67375/HCB-Z30MZMQ9-H</identifier><identifier type="DOI">10.1007/3-540-59338-1_41</identifier><identifier type="ChapterID">18</identifier><identifier type="ChapterID">Chap18</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 1995</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, 1995</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-Z30MZMQ9-H/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 002199 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002199 | 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:91F30B6F2190128B051C37FC2C7CEA0C0DA04F16
|texte= Linear logic with isabelle: Pruning the proof search tree
}}
| This area was generated with Dilib version V0.6.33. |  |