IG-Resolution for Definite Theories

Zbigniew Stachniak

In this paper we describe a general-purpose first-order automated reasoning framework based on the notion of a definite formula. The proposed reasoning framework consists of the first-order definite formula syntax and of a resolution-based procedure for automated reasoning with theories of definite formulas. Its propositional fragment is described in [1].

Definite formulas are certain well-formed expressions defined in terms of polarity. These formulas are not required to be in any specific syntactic normal form. From the semantic point of view, however, definite formulas are analogues of Horn clauses. Since the notion of polarity is readily available to nonclassical logics, the proposed framework allows a universal Horn clause-like representation of knowledge for classical as well as a range of non-classical logical systems.

In this paper we develop a non-clausal variant of SLD-resolution for reasoning with theories of definite formulas in classical as well as in some non-classical first-order logics. We describe a class of first-order logics for which this variant of resolution, called in this paper IG-resolution, is refutationally sound and complete. For classical logic, IG-resolution is an extension of SLD-resolution from Horn clauses to definite formulas. For non-classical logics, IG-resolution opens up the door for the construction of logic programming systems for definite formula fragments of these logics.

References

[1 ] Stachniak, Z.: Non-Clausal Reasoning with Propositional Definite Theories, in Proceedings of the Int. Conf. on Artificial Intelligence and Symbolic Computation, Lecture Notes in Artificial Intelligence, Springer-Verlag, 1476 (1998), 296–307.

Address: Department of Computer Science, York University, Toronto, Ontario, M3J 1P3 Canada

E-mail: zbigniew@cs.yorku.ca