Formulae-as-Resources Management for an Intuitionistic Theorem Prover - Archive ouverte HAL Access content directly
Conference Papers Year : 1998

Formulae-as-Resources Management for an Intuitionistic Theorem Prover

Didier Galmiche
Dominique Larchey-Wendling


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.
Not file

Dates and versions

inria-00098599 , version 1 (25-09-2006)


  • HAL Id : inria-00098599 , version 1


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. ⟨inria-00098599⟩
48 View
0 Download


Gmail Facebook Twitter LinkedIn More