Sciweavers

Share
CADE
2005
Springer

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic

9 years 3 months ago
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic
We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the prover concern resource management and focused derivations, both of which are traditionally understood in the domain of backward reasoning systems such as logic programming. We illustrate how resource management, focusing, and other intrinsic properties of linear connectives affect the basic forward operations of rule application, contraction, and forward subsumption. We also present some preliminary experimental results obtained with our implementation.
Kaustuv Chaudhuri, Frank Pfenning
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Kaustuv Chaudhuri, Frank Pfenning
Comments (0)
books