Carnegie Mellon University
file.pdf (389.5 kB)
Download file

Principles of Constructive Provability Logic (CMU-CS-10-151)

Download (389.5 kB)
journal contribution
posted on 2001-01-01, 00:00 authored by Robert J. Simmons, Bernardo Toninho

We present a novel formulation of the modal logic CPL, a constructive logic of provability that is closely connected to the Godel-L ¨ ob logic of provability. Our logical formulation allows modal ¨ operators to talk about both provability and non-provability of propositions at reachable worlds. We are interested in the applications of CPL to logic programming; however, this report focuses on the presentation of a minimal fragment (in the sense of minimal logic) of CPL and on the formalization of minimal CPL and its metatheory in the Agda programming language. We present both a natural deduction system and a sequent calculus for minimal CPL and show that the presentations are equivalent.