Implication of clauses is undecidable (Q1110493): Difference between revisions

The author studies the decision problems on implication of clauses in automated deduction systems. The implication \(A\Rightarrow B\) of two clauses A and B is interpreted as the formula \((\forall x_ 1...x_ nA)\Rightarrow (\forall y_ 1...y_ mB)\). Hence, clause A implies clause B iff \(A\wedge \neg B\) is not satisfiable. The clause implication problem is equivalent to the problem whether or not the class of clause sets consisting of one clause A and some ground unit clauses \(B_ i\) is decidable. Using the undecidability of finitely generated stable transitive relations on free terms, the author shows that: (1) \(A\Rightarrow B\) is decidable provided A is a 2-clause; (2) \(A\Rightarrow B\) is undecidable if A is a clause with four or more literals. (3) If A has at most three literals, then it remains an open question to decide \(A\Rightarrow B\).