Constructive Provability Logic
Logic in Computer Science
2012-05-30 v1 Programming Languages
Abstract
We present constructive provability logic, an intuitionstic modal logic that validates the L\"ob rule of G\"odel and L\"ob's provability logic by permitting logical reflection over provability. Two distinct variants of this logic, CPL and CPL*, are presented in natural deduction and sequent calculus forms which are then shown to be equivalent. In addition, we discuss the use of constructive provability logic to justify stratified negation in logic programming within an intuitionstic and structural proof theory.
Cite
@article{arxiv.1205.6402,
title = {Constructive Provability Logic},
author = {Robert J. Simmons and Bernardo Toninho},
journal= {arXiv preprint arXiv:1205.6402},
year = {2012}
}
Comments
Extended version of IMLA 2011 submission of the same title