Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic
Identifieur interne : 002079 ( Istex/Corpus ); précédent : 002078; suivant : 002080Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic
Auteurs : Didier Galmiche ; Dominique Larchey-WendlingSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In this paper, we present a new system for proof-search in propositional intuitionistic logic from which an efficient implementation based on structural sharing is naturally derived. The way to solve the problem of formula duplication is not based on logical solutions but on an appropriate representation of sequents with a direct impact on sharing and therefore on the implementation. Then, the proof-search is based on a finer control of the resources and has a O(n log n)-space complexity. The system has the subformula property and leads to an algorithm that, for a given sequent, constructs a proof or generates a counter-model.
Url:
DOI: 10.1007/3-540-46674-6_10
Links to Exploration step
ISTEX:8D58C2B4BEFF81AC34C83BB36DED724A5B996B25Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation><mods:affiliation>Vandœuvre-lès-Nancy, BP 239, France</mods:affiliation></affiliation></author><author><name sortKey="Larchey Wendling, Dominique" sort="Larchey Wendling, Dominique" uniqKey="Larchey Wendling D" first="Dominique" last="Larchey-Wendling">Dominique Larchey-Wendling</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:8D58C2B4BEFF81AC34C83BB36DED724A5B996B25</idno><date when="1999" year="1999">1999</date><idno type="doi">10.1007/3-540-46674-6_10</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-560489LD-4/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002079</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002079</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation><mods:affiliation>Vandœuvre-lès-Nancy, BP 239, France</mods:affiliation></affiliation></author><author><name sortKey="Larchey Wendling, Dominique" sort="Larchey Wendling, Dominique" uniqKey="Larchey Wendling D" first="Dominique" last="Larchey-Wendling">Dominique Larchey-Wendling</name></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="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: In this paper, we present a new system for proof-search in propositional intuitionistic logic from which an efficient implementation based on structural sharing is naturally derived. The way to solve the problem of formula duplication is not based on logical solutions but on an appropriate representation of sequents with a direct impact on sharing and therefore on the implementation. Then, the proof-search is based on a finer control of the resources and has a O(n log n)-space complexity. The system has the subformula property and leads to an algorithm that, for a given sequent, constructs a proof or generates a counter-model.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Didier Galmiche</name><affiliations><json:string>Vandœuvre-lès-Nancy, BP 239, France</json:string></affiliations></json:item><json:item><name>Dominique Larchey-Wendling</name></json:item></author><arkIstex>ark:/67375/HCB-560489LD-4</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: In this paper, we present a new system for proof-search in propositional intuitionistic logic from which an efficient implementation based on structural sharing is naturally derived. The way to solve the problem of formula duplication is not based on logical solutions but on an appropriate representation of sequents with a direct impact on sharing and therefore on the implementation. Then, the proof-search is based on a finer control of the resources and has a O(n log n)-space complexity. The system has the subformula property and leads to an algorithm that, for a given sequent, constructs a proof or generates a counter-model.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>102</abstractWordCount><abstractCharCount>644</abstractCharCount><keywordCount>0</keywordCount><score>8.224</score><pdfWordCount>5924</pdfWordCount><pdfCharCount>26848</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>12</pdfPageCount><pdfPageSize>431 x 666 pts</pdfPageSize></qualityIndicators><title>Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title><chapterId><json:string>10</json:string><json:string>Chap10</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>1999</copyrightDate><issn><json:string>0302-9743</json:string></issn><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor></serie><host><title>Advances in Computing Science — ASIAN’99</title><language><json:string>unknown</json:string></language><copyrightDate>1999</copyrightDate><doi><json:string>10.1007/3-540-46674-6</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-46674-1</json:string></eisbn><bookId><json:string>3-540-46674-6</json:string></bookId><isbn><json:string>978-3-540-66856-5</json:string></isbn><volume>1742</volume><pages><first>101</first><last>112</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>P. S. Thiagarajan</name><affiliations><json:string>Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, 600 017, Chennai, India</json:string><json:string>E-mail: pst@smi.ernet.in</json:string></affiliations></json:item><json:item><name>Roland Yap</name><affiliations><json:string>School of Computing, National University of Singapore, Lower Kent Ridge Road, 119260, Singapore</json:string><json:string>E-mail: ryap@comp.nus.edu.sg</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Computer Communication Networks</value></json:item><json:item><value>Special Purpose and Application-Based Systems</value></json:item><json:item><value>Programming Languages, Compilers, Interpreters</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-560489LD-4</json:string></ark><publicationDate>1999</publicationDate><copyrightDate>1999</copyrightDate><doi><json:string>10.1007/3-540-46674-6_10</json:string></doi><id>8D58C2B4BEFF81AC34C83BB36DED724A5B996B25</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-560489LD-4/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-560489LD-4/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-560489LD-4/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="1999">1999</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">Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title><author><persName><forename type="first">Didier</forename><surname>Galmiche</surname></persName><affiliation><address><postBox>BP 239</postBox><street>Vandœuvre-lès-Nancy</street><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Dominique</forename><surname>Larchey-Wendling</surname></persName></author><idno type="istex">8D58C2B4BEFF81AC34C83BB36DED724A5B996B25</idno><idno type="ark">ark:/67375/HCB-560489LD-4</idno><idno type="DOI">10.1007/3-540-46674-6_10</idno></analytic><monogr><title level="m" type="main">Advances in Computing Science — ASIAN’99</title><title level="m" type="sub">5th Asian Computing Science Conference Phuket, Thailand, December 10–12,1999 Proceedings</title><title level="m" type="part">Regular Papers</title><idno type="DOI">10.1007/3-540-46674-6</idno><idno type="book-id">3-540-46674-6</idno><idno type="ISBN">978-3-540-66856-5</idno><idno type="eISBN">978-3-540-46674-1</idno><idno type="chapter-id">Chap10</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">P.</forename><forename type="first">S.</forename><surname>Thiagarajan</surname></persName><email>pst@smi.ernet.in</email><affiliation><orgName type="institution">Chennai Mathematical Institute</orgName><address><street>92 G.N. Chetty Road, T. Nagar</street><settlement>Chennai</settlement><postCode>600 017</postCode><country key="IN">INDIA</country></address></affiliation></editor><editor><persName><forename type="first">Roland</forename><surname>Yap</surname></persName><email>ryap@comp.nus.edu.sg</email><affiliation><orgName type="department">School of Computing</orgName><orgName type="institution">National University of Singapore</orgName><address><street>Lower Kent Ridge Road</street><country key="SG">SINGAPORE</country><postCode>119260</postCode></address></affiliation></editor><imprint><biblScope unit="vol">1742</biblScope><biblScope unit="page" from="101">101</biblScope><biblScope unit="page" to="112">112</biblScope><biblScope unit="chapter-count">41</biblScope><biblScope unit="part-chapter-count">28</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName><affiliation><orgName type="institution">Karlsruhe University</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><settlement>NY</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Jan</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName><affiliation><orgName type="institution">Utrecht University</orgName><address><country key=""></country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>In this paper, we present a new system for proof-search in propositional intuitionistic logic from which an efficient implementation based on structural sharing is naturally derived. The way to solve the problem of formula duplication is not based on logical solutions but on an appropriate representation of sequents with a direct impact on sharing and therefore on the implementation. Then, the proof-search is based on a finer control of the resources and has a <hi rend="italic">O</hi>(<hi rend="italic">n</hi> log <hi rend="italic">n</hi>)-space complexity. The system has the subformula property and leads to an algorithm that, for a given sequent, constructs a proof or generates a counter-model.</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>I1603X</label><item><term type="Secondary" subtype="priority-1">Logics and Meanings of Programs</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-2">Mathematical Logic and Formal Languages</term></item><label>I13022</label><item><term type="Secondary" subtype="priority-3">Computer Communication Networks</term></item><label>I13030</label><item><term type="Secondary" subtype="priority-4">Special Purpose and Application-Based Systems</term></item><label>I14037</label><item><term type="Secondary" subtype="priority-5">Programming Languages, Compilers, Interpreters</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-560489LD-4/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><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><City>NY</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-46674-6</BookID><BookTitle>Advances in Computing Science — ASIAN’99</BookTitle><BookSubTitle>5th Asian Computing Science Conference Phuket, Thailand, December 10–12,1999 Proceedings</BookSubTitle><BookVolumeNumber>1742</BookVolumeNumber><BookSequenceNumber>1742</BookSequenceNumber><BookDOI>10.1007/3-540-46674-6</BookDOI><BookTitleID>64244</BookTitleID><BookPrintISBN>978-3-540-66856-5</BookPrintISBN><BookElectronicISBN>978-3-540-46674-1</BookElectronicISBN><BookChapterCount>41</BookChapterCount><BookHistory><OnlineDate><Year>1999</Year><Month>11</Month><Day>19</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>1999</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I1603X" Priority="1" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I13022" Priority="3" Type="Secondary">Computer Communication Networks</BookSubject><BookSubject Code="I13030" Priority="4" Type="Secondary">Special Purpose and Application-Based Systems</BookSubject><BookSubject Code="I14037" Priority="5" Type="Secondary">Programming Languages, Compilers, Interpreters</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>P.</GivenName><GivenName>S.</GivenName><FamilyName>Thiagarajan</FamilyName></EditorName><Contact><Email>pst@smi.ernet.in</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Roland</GivenName><FamilyName>Yap</FamilyName></EditorName><Contact><Email>ryap@comp.nus.edu.sg</Email></Contact></Editor><Affiliation ID="Aff4"><OrgName>Chennai Mathematical Institute</OrgName><OrgAddress><Street>92 G.N. Chetty Road, T. Nagar</Street><City>Chennai</City><Postcode>600 017</Postcode><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgDivision>School of Computing</OrgDivision><OrgName>National University of Singapore</OrgName><OrgAddress><Street>Lower Kent Ridge Road</Street><Country>Singapore</Country><Postcode>119260</Postcode></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Regular Papers</PartTitle><PartChapterCount>28</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-46674-6</BookID><BookTitle>Advances in Computing Science — ASIAN’99</BookTitle></PartContext></PartInfo><Chapter ID="Chap10" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>10</ChapterID><ChapterDOI>10.1007/3-540-46674-6_10</ChapterDOI><ChapterSequenceNumber>10</ChapterSequenceNumber><ChapterTitle Language="En">Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</ChapterTitle><ChapterFirstPage>101</ChapterFirstPage><ChapterLastPage>112</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>1999</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>1999</Year><Month>11</Month><Day>18</Day></RegistrationDate><OnlineDate><Year>1999</Year><Month>11</Month><Day>19</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><PartID>2</PartID><BookID>3-540-46674-6</BookID><BookTitle>Advances in Computing Science — ASIAN’99</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Didier</GivenName><FamilyName>Galmiche</FamilyName></AuthorName></Author><Author><AuthorName DisplayOrder="Western"><GivenName>Dominique</GivenName><FamilyName>Larchey-Wendling</FamilyName></AuthorName></Author><Affiliation ID="Aff6"><OrgAddress><Postbox>BP 239</Postbox><Street>Vandœuvre-lès-Nancy</Street><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>In this paper, we present a new system for proof-search in propositional intuitionistic logic from which an efficient implementation based on structural sharing is naturally derived. The way to solve the problem of formula duplication is not based on logical solutions but on an appropriate representation of sequents with a direct impact on sharing and therefore on the implementation. Then, the proof-search is based on a finer control of the resources and has a <Emphasis Type="Italic">O</Emphasis>(<Emphasis Type="Italic">n</Emphasis> log <Emphasis Type="Italic">n</Emphasis>)-space complexity. The system has the subformula property and leads to an algorithm that, for a given sequent, constructs a proof or generates a counter-model.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic</title></titleInfo><name type="personal"><namePart type="given">Didier</namePart><namePart type="family">Galmiche</namePart><affiliation>Vandœuvre-lès-Nancy, BP 239, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Larchey-Wendling</namePart><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">1999</dateIssued><copyrightDate encoding="w3cdtf">1999</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: In this paper, we present a new system for proof-search in propositional intuitionistic logic from which an efficient implementation based on structural sharing is naturally derived. The way to solve the problem of formula duplication is not based on logical solutions but on an appropriate representation of sequents with a direct impact on sharing and therefore on the implementation. Then, the proof-search is based on a finer control of the resources and has a O(n log n)-space complexity. The system has the subformula property and leads to an algorithm that, for a given sequent, constructs a proof or generates a counter-model.</abstract><relatedItem type="host"><titleInfo><title>Advances in Computing Science — ASIAN’99</title><subTitle>5th Asian Computing Science Conference Phuket, Thailand, December 10–12,1999 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">P.</namePart><namePart type="given">S.</namePart><namePart type="family">Thiagarajan</namePart><affiliation>Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, 600 017, Chennai, India</affiliation><affiliation>E-mail: pst@smi.ernet.in</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Roland</namePart><namePart type="family">Yap</namePart><affiliation>School of Computing, National University of Singapore, Lower Kent Ridge Road, 119260, Singapore</affiliation><affiliation>E-mail: ryap@comp.nus.edu.sg</affiliation><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">1999</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="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I13022">Computer Communication Networks</topic><topic authority="SpringerSubjectCodes" authorityURI="I13030">Special Purpose and Application-Based Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I14037">Programming Languages, Compilers, Interpreters</topic></subject><identifier type="DOI">10.1007/3-540-46674-6</identifier><identifier type="ISBN">978-3-540-66856-5</identifier><identifier type="eISBN">978-3-540-46674-1</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">64244</identifier><identifier type="BookID">3-540-46674-6</identifier><identifier type="BookChapterCount">41</identifier><identifier type="BookVolumeNumber">1742</identifier><identifier type="BookSequenceNumber">1742</identifier><identifier type="PartChapterCount">28</identifier><part><date>1999</date><detail type="part"><title>Regular Papers</title></detail><detail type="volume"><number>1742</number><caption>vol.</caption></detail><extent unit="pages"><start>101</start><end>112</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 1999</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1999</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 1999</recordOrigin></recordInfo></relatedItem><identifier type="istex">8D58C2B4BEFF81AC34C83BB36DED724A5B996B25</identifier><identifier type="ark">ark:/67375/HCB-560489LD-4</identifier><identifier type="DOI">10.1007/3-540-46674-6_10</identifier><identifier type="ChapterID">10</identifier><identifier type="ChapterID">Chap10</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 1999</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, 1999</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-560489LD-4/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 002079 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002079 | 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:8D58C2B4BEFF81AC34C83BB36DED724A5B996B25
|texte= Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic
}}
| This area was generated with Dilib version V0.6.33. |  |