×

Calculus of classical proofs. I. (English) Zbl 0890.03028

Shyamasundar, R. K. (ed.) et al., Advances in computing science - ASIAN ’97. 3rd Asian computing science conference, Kathmandu, Nepal, December 9–11, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1345, 321-335 (1997).
Summary: We introduce a simple natural deduction system of classical propositional logic called \(\lambda^v_{exc}\), and prove the computational properties of the system based on a call-by-value strategy. We show (1) a strict fragment of \(\lambda^v_{exc}\) that is complete with respect to classical provability, and the computational meaning of the existence of such a fragment; (2) a simple exit mechanism by the use of a proof of Peirce’s law, and some examples using classical proofs as programs; (3) the Church-Rosser property; (4) the CPS-translation from \(\lambda^v_{exc}\) to \(\lambda^\to\), and its correctness with respect to conversions; (5) a computational use of the logical inconsistency in \(\lambda^v_{exc}\), extended with a certain signature.
For the entire collection see [Zbl 0878.00079].

MSC:

03F03 Proof theory in general (including proof-theoretic semantics)
03B05 Classical propositional logic
03B70 Logic in computer science
PDFBibTeX XMLCite