An Intuitionistic Predicate Logic Theorem Prover
Open Access
- 1 October 1992
- journal article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 2 (5) , 619-656
- https://doi.org/10.1093/logcom/2.5.619
Abstract
A complete theorem prover for intuitionistic predicate logic based on the cut-free sequent calculue is presented. It includes a treatment of ‘quasi-free’ identity based on a delay mechanism and a special form of unification. Several fairly far-reaching optimizations of the basic algorithm essential to its performance are introduced. The paper concludes with a set of benchmarks and execution data which may facilitate a comparison of algorithms for intuitionistic logic. The system is available in source code from SICS.Keywords
This publication has 0 references indexed in Scilit: