LambdaMu-PRL - A Proof Refinement
Calculus for Classical Reasoning in Computational Type Theory
|
||
Nuria Brede, Christoph Kreitz. | ||
Technical Report, Universität Potsdam, March 2009. |
||
Abstract |
||
We present a hybrid proof calculus LambdaMu-PRL that combines the
propositional fragment of computational type theory with classical reasoning
rules from the LambdaMu-calculi. The calculus supports the top-down
development of proofs as well as the extraction of proof terms in a functional
programming language extended by a nonconstructive binding operator.
It enables a user to employ a mix of constructive and classical reasoning
techniques and to extract algorithms from proofs of specification theorems
that are fully executable if classical arguments occur only in proof parts
related to the validation of the algorithm.
We prove the calculus sound and complete for classical propositional logic,
introduce the concept of mu--safe terms to identify proof terms
corresponding to constructive proofs and show that the restriction of
LambdaMu-PRL to mu-safe proof terms is sound and complete for
intuitionistic propositional logic. We also show that an extension of
LambdaMu-PRL to arithmetical and first-order expressions is isomorphic
to Murthy's calculus PROG_K.
|
![]() Back to overview of papers |
|||
Bibtex Entry |
|||
@TechReport{tr:Allen+02a, author = "Nuria Brede and Christoph Kreitz", title = "$\lambda\mu$PRL -- A Proof Refinement Calculus for Classical Reasoning in Computational Type Theory", institution = "Institut f{\"u}r Informatik, Universit{\"a}t Potsdam", year = "2009" } |