Normal Natural Deduction Proofs (in classical logic)
Authors: Sieg, W.; Byrnes, J.
Source: Studia Logica, Volume 60, Number 1, January 1998 , pp. 67-106(40)
Abstract:Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation.
Document Type: Regular Paper
Affiliations: Department of Philosophy Carnegie Mellon University Pittsburgh, PA 15213-3891
Publication date: January 1, 1998