Open Learning Initiative

Sieg, W., Cittadini, S. (2005) Normal natural deduction proofs (in non-classical logics).  Mechanizing Mathematical Reasoning, LNAI 2005, 169-191.

Read research paper (pdf)

Abstract

We provide a theoretical framework that allows the direct search for natural deduction proofs in some non-classical logics, namely, intuitionistic sentential and predicate logic, but also in the modal logic S4.  The framework uses so-called intercalation calculi to build up broad search spaces from which normal proofs can be extracted, if a proof exists at all.