🚀 go-pugleaf

From article <TORKEL.92Oct4080150@bast.sics.se>, by torkel@sics.se (Torkel Franzen):
> 
>   Since Alfred Horn and preservation theorems are apparently not
> universally familiar even among those who subsist largely on a crunchy
> diet of Horn clauses, some further remarks are clearly in order.
> 
>   Hear ye, hear ye. This is the tale of the Horn clause, as it has come
> down to us from the masters of old.
> 

Can you, or anybody else, tell us the tale of (hereditary) Harrop
formulas?

Here is why I ask the question:

Horn formulas are a nice start for logic programming because they
yield a so nice model-theoretic denotational semantics, and because
they are so like grammar rules, rewriting rules, production rules,
whatever simple rules.  A major result has not yet been mentioned:
every definable relation can be defined using only Horn formulas.
---> A computer scientist cannot but love them :-)

Harrop formulas are nice for more logic programming because they are a
superset of Horn formulas and they yield a so nice proof-theoretic
operational semantics, and because they are so like sequent calculus
deduction rules, typing rules, whatever less simple rules.  
---> A computer scientist cannot but love them more :-)

There is a model-theoretic semantics for logic programming with Harrop
formulas, also not so nice as for Horn clauses.

This thread started with a beginner asking general questions.  I only
wish we do not give only answers of a fifteen years old state of the
art.  (Fifteen is for logic programming.  For logic it is more, but it
is OK there.)

Olivier Ridoux