David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
Jack Alan Reynolds
Learn more about PhilPapers
The history of building automated theorem provers for higher-order logic is almost as old as the field of deduction systems itself. The first successful attempts to mechanize and implement higher-order logic were those of Huet  and Jensen and Pietrzykowski . They combine the resolution principle for higher-order logic (first studied in ) with higher-order unification. The unification problem in typed λ-calculi is much more complex than that for first-order terms, since it has to take the theory of αβη-equality into account. As a consequence, the higher-order unification problem is undecidable and sets of solutions need not even always have most general elements that represent them. Thus the mentioned calculi for higher-order logic have take special measures to circumvent the problems posed by the theoretical complexity of higher-order unification. In this paper, we will exemplify the methods and proof- and model-theoretic tools needed for extending first-order automated theorem proving to higherorder logic. For the sake of simplicity take the tableau method as a basis (for a general introduction to first-order tableaux see part I.1) and discuss the higherorder tableau calculi HT and HTE first presented in . The methods in this paper also apply to higher-order resolution calculi [1, 13, 6] or the higher-order matings method of Peter , which extend their first-order counterparts in much the same way. Since higher-order calculi cannot be complete for the standard semantics by Gödel’s incompleteness theorem , only the weaker notion of Henkin models  leads to a meaningful notion of completeness in higher-order logic. It turns out that the calculi in [1, 13, 3, 19] are not Henkin-complete, since they fail to capture the extensionality principles of higher-order logic. We will characterize the deductive power of our calculus HT (which is roughly equivalent to these calculi) by the semantics of functional Σ-models. To arrive at a calculus that is complete with respect to Henkin models, we build on ideas from  and augment HT with tableau construction rules that use the extensionality principles in a goal-oriented way..
|Keywords||No keywords specified (fix it)|
|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
No citations found.
Similar books and articles
Jaakko Hintikka (2009). A Proof of Nominalism: An Exercise in Successful Reduction in Logic. In A. Hieke & H. Leitgeb (eds.), Reduction - Abstraction - Analysis. Ontos
Stephen G. Pulman (1997). Higher Order Unification and the Interpretation of Focus. Linguistics and Philosophy 20 (1):73-115.
Michael Kohlhase (1999). Higher-Order Multi-Valued Resolution. Journal of Applied Non-Classical Logics 9 (4):455-477.
Ortrun Ibens (2002). Connection Tableau Calculi with Disjunctive Constraints. Studia Logica 70 (2):241 - 270.
S. Awodey & C. Butz (2000). Topological Completeness for Higher-Order Logic. Journal of Symbolic Logic 65 (3):1168-1182.
Christoph Benzmüller, Chad E. Brown & Michael Kohlhase (2004). Higher-Order Semantics and Extensionality. Journal of Symbolic Logic 69 (4):1027 - 1088.
Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.
Added to index2009-04-20
Total downloads81 ( #59,022 of 1,902,527 )
Recent downloads (6 months)1 ( #452,252 of 1,902,527 )
How can I increase my downloads?