David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
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)|
|Through your library||Only published papers are available at libraries|
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 downloads9 ( #126,840 of 1,012,724 )
Recent downloads (6 months)1 ( #64,884 of 1,012,724 )
How can I increase my downloads?