Non-Clausal Reasoning with Definite Theories

Article type: Research Article

Authors: Stachniak, Zbigniew

Affiliations: Department of Computer Science, York University, Toronto, Canada

Abstract: In this paper we propose a general-purpose first-order automated reasoning framework based on the notion of a definite formula and on a non-clausal variant of SLD-resolution. This framework provides a universal Horn clause-like representation of knowledge for classical as well as a range of non-classical first-order logics. It provides a resolution-style method for automated reasoning with theories of definite formulas.

Keywords: automated reasoning, non-clausal resolution, definite formula

Journal: Fundamenta Informaticae, vol. 48, no. 4, pp. 363-388, 2001