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||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Dag 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.
Added to index2009-01-28
Total downloads20 ( #68,257 of 722,935 )
Recent downloads (6 months)2 ( #36,864 of 722,935 )
How can I increase my downloads?