Online research in philosophy

Different researchers use "the philosophy of automated theorem p r o v i n g " t o cover d i f f e r e n t concepts, indeed, different levels of concepts. Some w o u l d count such issues as h o w to e f f i c i e n t l y i n d e x databases as part of the philosophy of automated theorem p r o v i n g . Others wonder about whether f o r m u l a s should be represented as strings or as trees or as lists, and call this part of the philosophy of automated theorem p r o v i n g . Yet others concern themselves w i t h what k i n d o f search should b e embodied i n a n y automated theorem prover, or to what degree any automated theorem prover should resemble Prolog. Still others debate whether natural deduction or semantic tableaux or resolution is " b e t t e r " , a n d c a l l t h i s a part of the p h i l o s o p h y of automated theorem p r o v i n g . Some people wonder whether automated theorem p r o v i n g should be " h u m a n oriented" or "machine o r i e n t e d " — sometimes arguing about whether the internal p r o o f methods should be " h u m a n - I i k e " or not, sometimes arguing about whether the generated proof should be output in a f o r m u n d e r s t a n d a b l e by p e o p l e , and sometimes a r g u i n g a b o u t the d e s i r a b i l i t y o f h u m a n intervention in the process of constructing a proof. There are also those w h o ask such questions as whether we s h o u l d even be concerned w i t h completeness or w i t h soundness of a system, or perhaps we should instead look at very efficient (but i n c o m p l e t e ) subsystems or look at methods of generating models w h i c h might nevertheless validate invalid arguments. A n d a l l of these have been v i e w e d as issues in the philosophy of automated theorem proving. Here, I w o u l d l i k e to step back from such i m p l e m e n t - ation issues and ask: " W h a t do we really think we are doing when we w r i t e an automated theorem prover?" My reflections are perhaps idiosyncratic, but I do think that they put the different researchers* efforts into a broader perspective, and give us some k i n d of handle on w h i c h directions we ourselves m i g h t w i s h to pursue when constructing (or extending) an automated theorem proving system. A logic is defined to be (i) a vocabulary and formation rules ( w h i c h tells us w h a t strings of symbols are w e l l - formed formulas in the logic), and ( i i ) a definition of ' p r o o f in that system ( w h i c h tells us the conditions under which an arrangement of formulas in the system constitutes a proof). Historically speaking, definitions of ' p r o o f have been given in various different manners: the most c o m m o n have been H i l b e r t - s t y l e ( a x i o m a t i c ) , Gentzen-style (consecution, or sequent), F i t c h - s t y l e (natural deduction), and Beth-style (tableaux)..

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.

It has been suggested that moods are higher order-dispositions. This proposal is considered, and various shortcomings uncovered. The notion of a higher-order disposition is replaced by the more general notion of a higher-order functional state. An account is given in which moods are higher-order functional states, and the overall system of moods is a higher-order functional description of the mind. This proposal is defended in two ways. First, it is shown to capture some central features of our pre-scientific conception of moods. Secondly, it is argued that the account is more likely to be psychologically realistic (in a sense to be defined) than accounts which are behaviourally equivalent, but which do not employ a hierarchy of functional descriptions. It is suggested that the hierarchical structure of the model mirrors a feature of the physical states that realise moods and emotions.

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.

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.

In this paper, we show that Higher{Order Coloured Uni cation { a form of uni cation developed for automated theorem proving { provides a general theory for modeling the interface between the interpretation process and other sources of linguistic, non semantic information. In particular, it provides the general theory for the Primary Occurrence Restriction which (Dalrymple et al., 1991)'s analysis called for.

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.

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.

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..