David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
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||Philosophy Logic Mathematical Logic and Foundations Computational Linguistics|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Wilfried Sieg & Clinton Field (2005). Automated Search for Gödel’s Proofs. Annals of Pure and Applied Logic 133 (1):319-338.
Charles Parsons (1999). 1999 Spring Meeting of the Association for Symbolic Logic. Bulletin of Symbolic Logic 5 (4):479-484.
Similar books and articles
Dag Prawitz (1965). 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.
Michel Parigot (1997). Proofs of Strong Normalisation for Second Order Classical Natural Deduction. Journal of Symbolic Logic 62 (4):1461-1479.
Neil Tennant (2002). Ultimate Normal Forms for Parallelized Natural Deductions. Logic Journal of the IGPL 10 (3):299-337.
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 downloads50 ( #97,524 of 1,925,764 )
Recent downloads (6 months)5 ( #187,096 of 1,925,764 )
How can I increase my downloads?