Off-campus access
Using PhilPapers from home?
Click here to configure this browser for off-campus access.
- Michael Kohlhase, Higher-Order Automated Theorem Proving.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 [13] and Jensen and Pietrzykowski [17]. They combine the resolution principle for higher-order logic (first studied in [1]) 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 [19]. The methods in this paper also apply to higher-order resolution calculi [1, 13, 6] or the higher-order matings method of Peter [3], 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 [11], only the weaker notion of Henkin models [12] 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 [6] and augment HT with tableau construction rules that use the extensionality principles in a goal-oriented way..
Similar books and articles
Symbolic logic is a marvelous thing. It allows for an explicit expression of existence, viz. by means of the existential quantifier, and by it only. This is the true gist in Quine’s slogan “to be is to be a value of a bound variable.” Accordingly, one can also formulate explicitly the thesis of nominalism in terms of such logic. What this thesis says is that all the values of existential quantifiers we need in our language are particular objects, not higher-order objects such as properties, relations, functions and sets. This requirement is satisfied by the first-order languages using the received first-order logic. The commonly used basic logic is therefore nominalistic. But this result does not tell anything, for the received first-order logic is far too weak to capture all we need in mathematics or science. According to conventional wisdom, we need for this purpose either higher-order logic or set theory. Now both of them deal with higher-order entities and hence violate the canons of nominalism. This does not refute nominalism, however. For I will show that both set theory and higher-order logic can be made dispensable by developing a more powerful first-order logic that can do the same job as they do. Moreover, there are very serious problems connected with both of them. This constitutes an additional reason for dispensing with them in the foundations of mathematics. I will show how we can do just that. But we obviously need a better first-order logic for the purpose. Hence my first task is to develop one. But is this a viable construal of the problem of nominalism? The very distinction between particular and higher-order entities might perhaps seem to be hard to capture in logical terms — harder than has been indicated so far. Logicians like Jouko Väänänen (2001) have emphasized the complexities involved in trying to distinguish first-order logic from higher-order logic..
Reading list
| Discuss | Edit | Categorize | My bibliography
| Export citation | Scholar | More options ...
| | Scholar | More options ... Higher order unification is a way of combining information (or equivalently, solving equations) expressed as terms of a typed higher order logic. A suitably restricted form of the notion has been used as a simple and perspicuous basis for the resolution of the meaning of elliptical expressions and for the interpretation of some non-compositional types of comparative construction also involving ellipsis. This paper explores another area of application for this concept in the interpretation of sentences containing intonationally marked focus, or various semantic constructs which are sensitive to focus.Similarities and differences between this approach, and theories using alternative semantics, structured meanings, or flexible categorial grammars, are described. The paper argues that the higher order unification approach offers descriptive advantages over these alternatives, as well as the practical advantage of being capable of fairly direct computational implementation.
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Other links: springerlink.com dx.doi.org jstor.org | Scholar | At my library | More options ...
| | Other links: springerlink.com dx.doi.org jstor.org | Scholar | At my library | More options ... This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin’s general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in this paper provides a basis for developing higherorder mechanizations for many non-classical logics.
No categories
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Scholar | More options ...
| | Scholar | More options ... Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo.
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Other links: jstor.org | Scholar | At my library | More options ...
| | Other links: jstor.org | Scholar | At my library | More options ... Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces- so -called "topological semantics." The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Other links: jstor.org repository.cmu.edu | Scholar | At my library | More options ...
| | Other links: jstor.org repository.cmu.edu | Scholar | At my library | More options ... First-order modal logic, in the usual formulations, is not suf- ficiently expressive, and as a consequence problems like Frege’s morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such difficulties can be addressed. But this machinery can also be thought of as part of a move to a full higher-order modal logic. In this paper we present a sketch of just such a higher-order modal logic: its formal semantics, and a proof procedure using tableaus. Naturally the tableau rules are not complete, but they are with respect to a Henkinization of the “true” semantics. We demonstrate the use of the tableau rules by proving one of the theorems involved in G¨ odel’s ontological argument, one of the rare instances in the literature where higher-order modal constructs have appeared. A fuller treatment of the material presented here is in preparation.
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Scholar | More options ...
| | Scholar | More options ... The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.
No categories
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Scholar | More options ...
| | Scholar | More options ... In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes.
No categories
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Scholar | At my library | More options ...
| | Scholar | At my library | More options ... We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typed-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews'higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional extensionality axioms.
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Other links: jstor.org | Scholar | At my library | More options ...
| | Other links: jstor.org | Scholar | At my library | More options ... Thus, despite the di culty of higher-order automated theorem proving, which has to deal with problems like the undecidability of higher-order uni - cation (HOU) and the need for primitive substitution, there are proof problems which lie beyond the capabilities of rst-order theorem provers, but instead can be solved easily by an higher-order theorem prover (HOATP) like Leo. This is due to the expressiveness of higher-order Logic and, in the special case of Leo, due to an appropriate handling of the extensionality principles (functional extensionality and extensionality on truth values).
Reading list
| Discuss | Edit | Categorize | My bibliography | Export citation | Scholar | More options ...
| | Scholar | More options ... Discussion of Michael Kohlhase, Higher-order automated theorem proving
 Back
All discussions
Start a new thread
|
There are no threads in this forum |
Nothing in this forum yet.
