Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic
Identifieur interne : 002318 ( Istex/Checkpoint ); précédent : 002317; suivant : 002319Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic
Auteurs : Didier Galmiche [France] ; 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
Affiliations:
Links toward previous steps (curation, corpus...)
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></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><idno type="wicri:Area/Istex/Curation">002051</idno><idno type="wicri:Area/Istex/Checkpoint">002318</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002318</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 wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>Vandœuvre-lès-Nancy, BP 239</wicri:regionArea><wicri:noRegion>BP 239</wicri:noRegion><wicri:noRegion>BP 239</wicri:noRegion></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><affiliations><list><country><li>France</li></country></list><tree><noCountry><name sortKey="Larchey Wendling, Dominique" sort="Larchey Wendling, Dominique" uniqKey="Larchey Wendling D" first="Dominique" last="Larchey-Wendling">Dominique Larchey-Wendling</name></noCountry><country name="France"><noRegion><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002318 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 002318 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Checkpoint
|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. |  |