Resolution in the Domain of Strongly Finite Logics

Article type: Research Article

Authors: Stachniak, Zbigniew^{a; b; *} | O’Hearn, Peter^{a; b; **}

Affiliations: [a] Department of Computer Science, York University, North York, Ontario M3J JP3, Canada | [b] Department of Computing and Information Science, Queen’s University, Kingston, Ontario K7L 3N6, Canada

Note: [*] Research supported by the Natural Sciences and Engineering Research Council of Canada under grant A9136.

Note: [**] Research supported by the Natural Sciences and Engineering Research Council of Canada Postgraduate Scholarship.

Abstract: In this paper the notion of a resolution counterpart of a propositional logic is introduced and studied. This notion is based on a generalization of the resolution rule of J.A. Robinson. It is shown that for every strongly finite logic a refutationally complete nonclausal resolution proof system can be constructed and that the completeness of such systems is preserved with respect to the polarity and set of support strategies.

DOI: 10.3233/FI-1990-13307

Journal: Fundamenta Informaticae, vol. 13, no. 3, pp. 333-351, 1990