Formulae-as-Resources Management for an Intuitionistic Theorem Prover

Didier Galmiche 1 Dominique Larchey-Wendling
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper outlines new concepts for an alternative implementation of the intuitionistic contraction-free LJT system (and consequently proof search) in imperative programming languages with a good and efficient management of formulae (as resources). Logic programming languages provide natural support to implement automated proof search, with no necessity to have explicit knowledge about the form and the number of formulae arising in LJT proofs. By the introduction of a new notion of subformula (and consequently of a subformula property) for the LJT system, we obtain interesting and usable results about the possible management of formulae in a proof. A derived structure (direct acyclic graph) including some sharing of subformulae is proposed to deal with formulae during the proof search and the application of logical rules. The based-on proof search method is independent of the possible strategies. Thus we obtain an efficient implementation of LJT in imperative programming languages based on management of formulae-as-resources.
Type de document :
Communication dans un congrès
5th Workshop on Logic, Language, Information and Computation - WoLLIC'98, 1998, Sao Paulo, Brazil, 6 p, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098599
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:53
Dernière modification le : mardi 24 avril 2018 - 13:34:43

Identifiants

  • HAL Id : inria-00098599, version 1

Collections

Citation

Didier Galmiche, Dominique Larchey-Wendling. Formulae-as-Resources Management for an Intuitionistic Theorem Prover. 5th Workshop on Logic, Language, Information and Computation - WoLLIC'98, 1998, Sao Paulo, Brazil, 6 p, 1998. 〈inria-00098599〉

Partager

Métriques

Consultations de la notice

74