Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic

Didier Galmiche 1 Dominique Larchey-Wendling 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 ${\cal 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.
Type de document :
Communication dans un congrès
P.S. Thiagarajan, R. Yap. Asian Computing Science Conference - ASIAN'99, 1999, Phuket, Thailand, Springer Verlag, 1742, pp.101-112, 1999, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00098992
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:03
Dernière modification le : mardi 24 avril 2018 - 13:34:45

Identifiants

  • HAL Id : inria-00098992, version 1

Collections

Citation

Didier Galmiche, Dominique Larchey-Wendling. Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic. P.S. Thiagarajan, R. Yap. Asian Computing Science Conference - ASIAN'99, 1999, Phuket, Thailand, Springer Verlag, 1742, pp.101-112, 1999, Lecture Notes in Computer Science. 〈inria-00098992〉

Partager

Métriques

Consultations de la notice

74