Calculus of Classical Proofs II

スポンサーリンク

概要

• 論文の詳細を見る

• We provide a simple natural deduction system of classical propositional logic called λ_<exc>, and demonstrate the proof-theoretical and computational properties of the system from a programming viewpoint. The introduction of λ_<exc> is a consequence of our observations on the existence of a special form of cut-free LK proofs, which we call LJK proofs with invariants. We first show the existence of LJK proofs with invariants for each tautology. On the basis of the proof-theoretical result, we then present(1)a strict fragment of λ_<exc> that is complete with respect to classical provability, (2)a translation from arbitrary proofs to LJK-style proofs, (3)the Church-Rosser and strong normalization properties of λ_<exc>, and (4)an isomorphism between Parigot's λμ-calculus and λ_<exc>, and a comparison with related work.

• 一般社団法人情報処理学会の論文
• 1998-12-15

著者

• FUJITA KEN-ETSU

  Faculty of Computer Science and Systems Engineering, Kyushu Institute of Technology

• Fujita Ken-etsu

  Faculty Of Computer Science And Systems Engineering Kyushu Institute Of Technology

関連論文

• μ-Head Form Proofs with at Most Two Formulas in the Succedent
• Calculus of Classical Proofs II

スポンサーリンク