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 the 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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. D’Agostino and D. Gabbay. A generalisation of analytic deduction via labelled deductive systems. Part I: Basic substructural Logics. Journal of Automated Reasoning, 13:243–281, 1994
K. Broda, A compiled labelled deductive system for propositional intuitionistic logic (full version) available from K. Broda, 1998.
K. Broda, M. Finger and A. Russo. Labelled Natural Deduction for Substructural Logics. Accepted, Journal of the International Group for Pure and Applied Logics.
K. Broda and A. Russo. A Unified Compilation Style Labelled Deductive System for Modal and Substructural Logic using Natural Deduction. Technical Report 10/97. Department of Computing, Imperial College 1997.
C. L. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press 1973.
M. Fitting. Proof Methods for Modal and Intuitionistic Logic. D. Reidel, 1983.
D. Gabbay. Labelled Deductive Systems, Volume I-Foundations. OUP, 1996
J. H. Gallier. Logic for Computer Science. Harper and Row, 1986.
H.J. Ohlbach. Semantics-based translation methods for modal logics. Journal of Logic and Computation, 1(5):691–746 1991.
J.A. Robinson. Logic, Form and Function. Edinburgh Press 1979.
A. Russo. Modal Logics as Labelled Deductive Systems. PhD. Thesis, Department of Computing, Imperial College, 1996.
R. A. Schmidt. Resolution is a decision procedure for many propositional modal logics. Advances in Modal Logic, Vol.1: 189–208, CSLI 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broda, K., Gabbay, D. (1999). CLDS for Propositional Intuitionistic Logic. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_10
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive