Constructive provability logic is the generic name for two families of modal logics. Both variants of constructive provability logic are broadly similar to Alex Simpson's intuitionistic Kripke semantics as presented in his thesis, "The Proof Theory and Semantics of Intuitionistic Modal Logic." Like constructive provability logic, the intuitionistic Kripke semantics is a set of logical principles describing the behavior of a hypothetical judgment. Within the framework of the logic's defining principles, various modal connectives can be defined by giving introduction and elimination rules that respect the defining principles.
The two variants of constructive provability logic can be distinguished by whether contradiction at an accessible world implies contradiction at the current world (whether ◊⊥ implies ⊥). In "tethered" constructive provability logic (or CPL), this is not the case: ◊⊥ does not imply ⊥. In "de-tethered" constructive provability logic (or CPL*), contradiction at any accessible world implies a contradiction at the current world.
The logic's presentation co-evolved with a formalization of the logic and its metatheory in the Agda proof assistant. All claimed results about the metatheory of constructive provability logic have been formalized in Agda, though the claimed connection between hybrid CPL* and logic programming with stratified negation has not been formalized.
Papers
Papers are listed in reverse chronological order.
-
Constructive Provability Logic.
Robert J. Simmons and Bernardo Toninho.
Submitted to the Journal of Logic and Computation's special issue on
Intuitionistic Modal Logics and Applications.
IMLA'11 did not have formal proceedings, so we reused the name. This article attempts to subsume the course report, tech report, and -
Constructive Provability Logic.
Robert J. Simmons and Bernardo Toninho.
Presented at the
Intuitionistic Modal Logics and Applications Workshop, July 2011.
Briefly presents both intuitionistic CPL and CPL*, and discusses their differences, especially in terms of what formulas are always valid in the two systems. Does not discuss the logic programming motivation at all. This is the briefest existing introduction to the logic and the only written discussion of de-tethered constructive provability logic. It therefore compliments the tech report (listed below), which goes into more detail about background and motivation while also providing more technical details of proofs. The Agda code associated with this paper is available here. -
Distributed Deductive Databases, Declaratively: The L10 logic programming
language.
Robert J. Simmons, Bernardo Toninho, and Frank Pfenning.
Short paper in the X10 workshop, June 2011.
An early attempt at designing a distributed logic programming language based on constructive provability logic (hybrid CPL* in particular). This paper does not go into detail about the connection with constructive provability logic, however, as certain formal aspects (such as the first-order extension of CPL*) have not been worked out in detail. -
Principles of Constructive Provability Logic.
Robert J. Simmons and Bernardo Toninho.
CMU Tech Report, December 2010.
Provides an detailed account of minimal CPL and its metatheory. A sequent calculus is presented along with a cut and identity theorem, and a natural deduction calculus is presented along with a substitution theorem. The two presentations are shown to be sound and complete with respect to each other. This is the most complete presentation of proofs that is in TeX and not in Agda. The Agda code associated with this paper is available here. - Logic Programming in
Constructive Provability Logic.
Robert J. Simmons and Bernardo Toninho.
Course project report, May 2010.
An initial investigation of CPL. Almost entirely superseded by later work.
Presentation
This is a presentation given at IMLA 2011 in Nancy, France on July 25, 2011. An earlier version of this presentation was given at CMU on May 11, 2011, and an extended version of this presentation was given at INRIA Saclay on July 26, 2011.