Krysia Broda, Dov Gabbay
The compilation approach for Labelled Deductive Systems (CLDS) is used to
obtain a decidable theorem prover for propositional intuitionistic logic.
Previous applications of the CLDS method were based around a natural deduction system, together with the notion of a theory as a structure of points, called a configuration,
and a semantic approach using a translation technique based on first-order logic. In this paper t same semantic method is used, but the proof system is instead a first order theorem prover using techniques drawn from the Davis Putnam and Hyper-resolution procedures. This is shown to be sound and complete with respect to the semantics. The resulting system is a generalisation of intuitionistic logic in a sense that is explained and it is briefly compared with other first order translation techniques.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.