Computer Science Department
School of Computer Science, Carnegie Mellon University


Principles of Constructive Proability Logic

Robert J. Simmons, Bernardo Toninho

December 2010

Proof Code

Keywords: Modal logic, probability logic, judgmental reconstruction, natural deduction, sequent calculus, constructive type theory

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
School of Computer Science

This page maintained by