The emptiness problem of one binary recursive horn clause is undecidable
Philippe Devienne, Patrick Lebègue, Jean-Christophe Routier · 1993
The simplest recursive program in Horn clause languages is of the form : 8 ? ! ? : p(fact) / : p(lef t) / p(right) : / p(goal) : This corresponds to append--like programs. The two most relevant problems concerning this class are the halting and the emptiness (existence of at least one solution) problems. The halting problem has been proved undecidable in the general case in [7]. Here we establish the undecidability of the emptiness problem in the general case. The (non--)linearity (each variable occurs at most once) of the terms fact, left, right and goal is crucial. We prove that as soon as three of them are linear, the emptiness problem becomes decidable. For the halting problem, the linearity of goal or left is sufficient. Moreover, the undecidability of the emptiness problem implies the unsatisfiability of the class of quantificational formulas with one 2-clause and two unit clauses which was opened for twenty years. 1 Introduction Quantificational formulas have been subject t...