David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 60 (1):67-106 (1998)
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||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
Similar books and articles
Dag Prawitz (1965/2006). Natural Deduction: A Proof-Theoretical Study. Dover Publications.
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Michel Parigot (1997). Proofs of Strong Normalisation for Second Order Classical Natural Deduction. Journal of Symbolic Logic 62 (4):1461-1479.
Sara Negri (2005). Proof Analysis in Modal Logic. Journal of Philosophical Logic 34 (5/6):507 - 544.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Andrzej Wiśniewski (2004). Socratic Proofs. Journal of Philosophical Logic 33 (3):299-326.
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.
Kosta Došen (2003). Identity of Proofs Based on Normalization and Generality. Bulletin of Symbolic Logic 9 (4):477-503.
A. S. Troelstra (1999). Marginalia on Sequent Calculi. Studia Logica 62 (2):291-303.
Added to index2009-01-28
Total downloads21 ( #68,657 of 1,088,372 )
Recent downloads (6 months)2 ( #42,603 of 1,088,372 )
How can I increase my downloads?