Normal natural deduction proofs (in classical logic)
Studia Logica 60 (1):67-106 (1998)
| 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. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,679 |
| External links |
  Try with proxy. Try with proxy. |
| Through your library | Configure |
Similar books and articlesDag Prawitz (1965/2006). Natural Deduction: A Proof-Theoretical Study. Dover Publications.
Kosta Došen (2003). Identity of Proofs Based on Normalization and Generality. Bulletin of Symbolic Logic 9 (4):477-503.
Ricardo Caferra, Stéphane Demri & Michel Herment (1993). A Framework for the Transfer of Proofs, Lemmas and Strategies From Classical to Non Classical Logics. Studia Logica 52 (2):197 - 232.
Andrzej Wiśniewski (2004). Socratic Proofs. Journal of Philosophical Logic 33 (3):299-326.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Sara Negri (2005). Proof Analysis in Modal Logic. Journal of Philosophical Logic 34 (5-6):507 - 544.
Michel Parigot (1997). Proofs of Strong Normalisation for Second Order Classical Natural Deduction. Journal of Symbolic Logic 62 (4):1461-1479.
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
A. S. Troelstra (1999). Marginalia on Sequent Calculi. Studia Logica 62 (2):291-303.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads18 ( #67,528 of 549,070 )Recent downloads (6 months)4 ( #19,186 of 549,070 )How can I increase my downloads? |
My notes
Discussion
