Fujita, Ken-etsu 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]. Cited in 1 Document MSC: 03F03 Proof theory in general (including proof-theoretic semantics) 03B05 Classical propositional logic 03B70 Logic in computer science Keywords:natural deduction system; classical propositional logic; computational properties; call-by-value strategy; classical provability; Peirce’s law; Church-Rosser property; CPS-translation; logical inconsistency PDFBibTeX XMLCite \textit{K.-e. Fujita}, Lect. Notes Comput. Sci. 1345, 321--335 (1997; Zbl 0890.03028)