Some Undecidable Classes of Clause Sets

Abstract

The undecidability of finitely generated stable transitive relations on free terms is proved in an elementary way and then used to show the undecidability of the implication A => B of two clauses A and B. The implication is decidable in the case A has at most two literals that are complementary unifiable after renaming. Application of the undecidability of transitive relations yields more classes of clause sets that have an undecidable satisfiability problem: clause sets consisting of two clauses with two literals each (2-clauses) and in addition 2 ground units, clause sets consisting of a single 3-clause and arbitrarily many (non-ground) units and clause sets consisting of a 4-clause and arbitrarily many ground units. Finally we show the undecidability of the so-called D-clause sets, where a D-clause is a Horn-clause of the form Q1(x1)^ . . .^ Qn(xn) => Qn+1(t).