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)

Publisher: Springer

Buy & download fulltext article:


Price: $47.00 plus tax (Refund Policy)


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

Related content


Free Content
Free content
New Content
New content
Open Access Content
Open access content
Subscribed Content
Subscribed content
Free Trial Content
Free trial content

Text size:

A | A | A | A
Share this item with others: These icons link to social bookmarking sites where readers can share and discover new web pages. print icon Print this page