[Zurück]

U. Egly:
"Embedding Lax Logic into Intuitionistic Logic";
Vortrag: International Conference on Automated Deduction (CADE), Copenhagen, Denmark; 27.07.2002 - 30.07.2002; in: "Proceedings of the 18th International Conference on Automated Deduction", a. voronkov (Hrg.); Springer Verlag, (2002), ISBN: 3-540-43931-5; S. 78 - 93.

Lax logic is obtained from intuitionistic logic by adding a single modality $\circ$ 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 $\lambda$-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.