SMALLEST HORN CLAUSE PROGRAMS

The simplest nontrivial program pattern in logic programming is the fo llowing:p(fact) <-- p(left) <-- p(right). <-- p(goal). where fact, goa l, left, and right are arbitrary terms. Because the well-known append program matches this pattern, we will denote such programs ''append-li ke.'' In spite of their simple appearance, we prove in this paper that termination and satisfiability (i.e., the existence of answer-substit utions, called the emptiness problem) for append-like programs are und ecidable. We also study some subcases depending on the number of occur rences of variables in fact, goal, left, or right. Moreover, we prove that the computational power of append-like programs is equivalent to the one of Turing machines; we show that there exists an append-like u niversal program. Thus, we propose an equivalent of the Bohm-Jacopini theorem for logic programming. This result confirms the expressiveness of logic programming. The proofs are based on program transformations and encoding of problems, unpredictable iterations within number theo ry defined by J. H. Conway, or the Post correspondence problem.