By Andrea Formisano
Università di Roma La Sapienza (consorzio Roma-L’Aquila)
March 24, 2000.
Abstract
Recently, several authors introduced various theory-based extensions of basic inference procedures (the resolution procedure and the connection method, among others). A common philosophy inspired all of these new proposals: to endow the automated systems with some sort of “human skill”; i.e., give the system the capacity of exploiting semantical knowledge behind its ability of performing syntactical manipulations of formulas. In these systems the reasoning activity develops at two distinct levels: a foreground level, where an essentially syntactical framework is employed, and a background level which is the repository of the semantic knowledge. In the case of T-resolution |just one among the various proposals| this knowledge takes the form of a decision procedure for the satis fiability of formulas of a underlying theory T which is a parameter of the whole system.
In this context, two main streams of research deserve deep investigation. Firstly, the properties of the T-resolution rule itself should be assessed. As an original contribution we present a technique a la Henkin for proving completeness of (generic) resolution-based calculi that avoids compactness assumptions. Then, the characteristics of the T-resolution procedure are analyzed in depth by considering its completeness, its mechanizability, and a number of its re nements. Secondly, we are interested in obtaining decidability results for speci c theories. As a starting point, we present a repository of decision methods for fragments of Set Theory. In particular, we devise an algorithm for deciding exists*forall sentences on sets with self-singleton atoms (following a proposal of Quine).
As a matter of fact, Set Theory is expressive enough to o er a rm ground for formalizing almost every mathematical concept. This argument motivates the e orts directed at characterizing its decidable fragments and at automating set-reasoning. As a contribution in this direction we give a reformulation of a number of rst-order theories within a homogeneous framework such as the Tarski-Chin-Givant map calculus. As a consequence, the automation of the map calculus would o er an alternative approach to theory-reasoning. In order to reach this goal, we start by tackling the problem of translatability between rst-order logic and map calculus; for instance, we show how the variety of (antithetic) possibilities o ered by axiomatic Set Theory can be forged within the map formalism. Then, we introduce the basics of map reasoning technology in order to set the ground for (a) the realization of a “stand-alone” platform for map reasoning, and (b) the implementation of a map reasoner on top of an existing rst-order theorem prover. Finally, we report on an initial experimentation activity that yields automated proofs of fundamental properties of our axiomatizations; we face the problem of singling out a series of tactics for automated detection of legal set-abstraction; and we outline an innovative and promising approach to the decision problem for syllogistics.