Normal Natural Deduction Proofs (in Non-classical Logics)
Sieg, W., Cittadini, S. (2005) Normal natural deduction proofs (in non-classical logics). Mechanizing Mathematical Reasoning, LNAI 2005, 169-191.
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.