CMU-CS-10-151 Computer Science Department School of Computer Science, Carnegie Mellon University
Principles of Constructive Proability Logic Robert J. Simmons, Bernardo Toninho December 2010
We present a novel formulation of the modal logic CPL, a constructive logic of provability that is closely connected to the Gödel-Löb 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. 37 pages
| |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |