Embedding Lax Logic into Intuitionistic Logic
- 295 Downloads
Lax logic is obtained from intuitionistic logic by adding a single modality o which captures properties of necessity and possibility. This modality was considered by Curry in two papers from 1952 and 1957 and rediscovered recently in different contexts like verification of circuits and the computational λ-calculus. We show that lax logic can be faithfully embedded into the underlying intuitionistic logic and discuss (computational) properties of the embedding. Using the proposed polynomial-time computable embedding, PSPACE-completeness of the provability problem of propositional lax logic is shown.
Unable to display preview. Download preview PDF.
- 3.H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957.Google Scholar
- 5.Uwe Egly. Embedding lax logic into intuitionistic logic. Technical report, Abteilung Wissensbasierte Systeme, TU Wien, 2002.Google Scholar
- 7.M. Fairtlough, M. Mendler, and M. Walton. First-order lax logic as a framework for constraint logic programming. Technical Report MIPS-9714, University of Passau, 1997.Google Scholar
- 8.M. Fairtlough and M. Walton. Quantified lax logic. Technical Report CS-97-11, University of Sheffield, Department of Computer Science, 1997.Google Scholar
- 9.D. Galmiche and D. Larchey-Wendling. Structural sharing and efficient proof-search in propositional intuitionistic logic. In Asian Computing Science Conference, ASIAN’99, volume 1742 of Lecture Notes in Computer Science, pages 101–112. Springer Verlag, 1999.Google Scholar
- 10.J. M. Howe. Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St Andrews, December 1998. Available as University of St Andrews Research Report CS/99/1.Google Scholar
- 11.J. M. Howe. Proof search in lax logic. Mathematical Structures in Computer Science, 11(4):573–588, August 2001.Google Scholar
- 13.M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993.Google Scholar
- 15.F. Pfenning and R. Davis. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511–540, August 2001.Google Scholar