Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic (Q1819946)

The computational complexity of the propositional Horn-clause logic is significant, since its satisfiability is decidable in polynomial time, although the satisfiability problem of the propositional logic is NP- complete. From the standpoint of NP-completeness, there have been many attempts to extend as much as possible the class of propositional formulae for which the satisfiability problem is in P. This paper is thought of as such an attempt. We propose a class of non-Horn sentences, for which the satisfiability problem is in P. To detect the satisfiability for such a class, we treat an extended version of linear layered resolution deduction based on input deductions, which is formed by repetitions of input deductions with derived unit clauses to be memorized.