Unit Resolution for a Subclass of the Ackermann Class

Abstract

The Ackermann class and the Gödel class are typical subclasses of pure first-order logic. The unsatisfiability problems for the Ackermann class and the Gödel class of formulas are decidable and resolution strategies to the unsatisfiability problems for the Ackermann class and the Gödel class were constructed by W. H. Joyner. Applying unit resolution of C. L. Chang, we construct a preprocessor to Joyner's resolution strategy for a subclass of the Ackermann class, since his strategy may necessitate too much time and space from the practical point of view. In this paper, we describe an algorithm to decide whether there is a unit resolution refutation from a set of clauses in a subclass ACK₂ of the Ackermann class, in which at most two literals with variables appear in each clause. In this algorithm, we represent the unit clause resolvents generated by unit resolution by means of finite automata. Also, we transform the decision problem of a unit resolution refutability for ACK₂ to the emptiness problem of intersections of two regular languages. We give the time complexity and the space complexity of the constructed algorithm. This result is an extension of the result by N. D. Jones namely that it can be decided in deterministic polynomial time whether or not ther is a unit resolution refutation for the propositional logic.