Computing Publications

Publications Home » A Compiled Labelled Deductive Sys...

A Compiled Labelled Deductive System for Propositional Intuitionistic Logic

Krysia Broda, Dov Gabbay

Conference or Workshop Paper
Tableaux 99, Saratoga Springs USA
June, 1999
Volume 1617
pp.66–81
Springer-Verlag
ISBN 3-540-67697-X
Abstract

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.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.