# Publication details

##
One binary Horn clause is enough

P. Devienne, P. Lebegue, J.C. Routier, Jörg Würtz

Symposium on Theoretical Aspects of Computer Science, pp. 21--32, Springer-Verlag, February 1994

This paper proposes an equivalent form of the famous Böhm-Jacopini theorem for
declarative languages. C. Böhm and G. Jacopini proved
that all programming can be done with at most one single
while-do. That result is cited
as a mathematical justification for structured programming. A similar result
can be shown for declarative programming. Indeed the simplest class of
recursive programs in Horn clause languages can be defined by the
following scheme:

A1 <-.
A2 <- A3.
<- A4.

that is:
* x1...xm (A1 (A2
A3)
A4)*
where Ai are positive first-order literals.
This class is shown here to be as expressive as Turing machines and
all simpler classes would be trivial. The proof is based on a
remarkable and not enough known codification of any computable
function by unpredictable iterations proposed by. Then, we prove
effectively by logical transformations
that all conjunctive formulas of Horn clauses can be translated into
an equivalent conjuctive 4-formula (as above). Some consequences are
presented in several contexts (mathematical logic, unification modulo
a set of axioms, compilation techniques and other program
patterns).
Download PDF
Show BibTeX

@INPROCEEDINGS{devienne:94,
title = {One binary Horn clause is enough},
author = {P. Devienne and P. Lebegue and J.C. Routier and J{\"o}rg W{\"u}rtz},
year = {1994},
month = {feb},
editor = {"P. Enjalbert, E.W. Mayr, K.W. Wagner"},
publisher = {"Springer-Verlag"},
booktitle = {Symposium on Theoretical Aspects of Computer Science},
series = {"Lecture Notes in Computer Science, vol. 775"},
pages = {"21--32"},
}

Login to edit

Legal notice, Privacy policy