Intuitionistic proof transformations and their application to constructive program synthesis

DOI10.1007/BFB0055908MaRDI QIDQ4217953zbMATH OpenFDO

Publication date 11 November 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055908

constructive proof cut rule cut-free proof transformation length of proofs matrix proof matrix-based theorem prover for first-order intuitionistic logic NUPRL program synthesis proofs as programs paradigm sequent proof

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The goal of program synthesis is to enable computers to generate computer programs, with two desirable consequences: relieving humans from the least creative aspects of code writing and generate programs that are proved correct. A classical approach to synthesis is based on the ``proofs as programs paradigm: given a specification of a program, generate a constructive proof of the existence of a function \(f\) that satisfies it, and extract from the proof a program computing \(f\). The constructive proof can be generated by using an interactive proof assistant such as NUPRL. Clearly, In is desirable to automate the generation of the proof as much as possible. For this purpose, the proof assistant may invoke a theorem prover to carry out the purely logical parts of the proof: in the working environment for this paper, NUPRL is coupled with a matrix-based theorem prover for first-order intuitionistic logic. This integration requires two translations: subgoals of the NUPRL proof need to be translated into problems for the matrix prover, and the matrix proofs need to be transformed into NUPRL sequent-style-proofs. The latter transformation is the topic of this paper. Two main issues with such a transformation are application of the cut rule and the length of proofs. If the cut rule is applied systematically, the resulting sequent proof may be very different from its original NUPRL context. Intuitively, this is because the cut rule introduces a synthetic character in proofs that would be otherwise analytic, where ``synthetic and ``analytic correspond, roughly speaking, to forward and backward reasoning. The first contribution of this paper is a cut-free transformation based on permutations. The length of proofs is also an issue, because one does not want the sequent proof to be too long with respect to the matrix proof. The second contribution of this paper is a negative result: the authors prove that the length of the sequent proof resulting from this cut-free transformation cannot be polynomially bounded by the length of the matrix proof. Cut-freeness and conciseness are at odds, and future work will consist in trying to design a trade-off, where a controlled usage of the cut rule allows to make proofs shorter. Being a conference paper, the article is technical, and not-self-contained. It will be useful to other researchers working on similar problems, but readers who are not already close to the topic should read first an introduction to sequent calculi and the related works cited in this paper. For the entire collection see [Zbl 0896.00032].

Recommendations

Cited in

(8)

Describes a project that uses

Uses Software

Nuprl

This page was built for publication: Intuitionistic proof transformations and their application to constructive program synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4217953)