RE: Rules are *not* Horn clauses!

> >Please notice that Prolog rules (as well as any other practical
> >computational rule concept such as SQL views and OCL implications)
> >are *not* Horn clauses! They are, for good reasons, more expressive,
> >allowing for negation in their body/antecedent (and other things,
> >such as quantifiers, as in the case of SQL views).
> 
> Maybe Prolog has morphed into something else since the last time I 
> looked at it. Can you characterize what subset of logic *is* captured 
> by Prolog? I'm not sure what you mean by 'allowing for negation'.

You probably know that Prolog, like SQL, applies a negation (in
rule bodies only) under the closed-world assumption, often called
negation-as-failure. A negation operator is essential for
expressing queries that arise in practical applications. For
being practically (and not just academically) relevant, rules
for the SemanticWeb need negation!

The model-theoretic semantics for logic programming rules with
negation (also called "normal logic programs") is given by
a certain definition of intended models (called "stable models").
There is an efficient inference operation, called "well-founded
semantics" that is sound, but not complete, wrt stable models.

> Ah, yes; SQL isnt what I would call a logical query language at all. 

But one may view SQL queries (without aggregates) as FOL formulas.
E.g., "SELECT x,y,z FROM p WHERE x=y" corresponds to the formula
"p(x,x,z)" which is answered by returning all bindings to x and z
such that the corresponding instantiations are entailed by the
current database state.

> >We should consider the concept of a rule as a basic one that
> >is not derived from that of a Horn clause (which happens to be
> >a very restricted/simplified type of rule). The concept of a
> >Horn clause is tight to classical (two-valued) logic. But rules
> >play a role in all kinds of formalism with a non-classical
> >logic semantics (such as intuitionistic, partial, temporal,
> >inconsistency-tolerant logic, etc.).
> 
> Hold on a minute there. There is no single notion of 'rule' that 
> plays a role in a variety of logics. 

Why not? For each logic (even if it does not have an implication) 
we can define the notion of a sequent F => G, where both F and G 
may be composite and have free variables, and using the logic's 
model theory, we can define when such a sequent is satisfied by 
a model. This seems to provide a generic concept of a rule.

> BTW, the notion of Horn clause is not restricted to classical 
> two-valued logic. It applies to any logic which has conjunction, 
> disjunction and negation, which includes all those you mention here 
> and many others.

I don't understand your remark. Isn't it essential for the
concept of a Horn clause that -p v q is equivalent to p -> q?
This equivalence does not hold, for instance, in intuitionistic
or partial logic.

-Gerd

Received on Wednesday, 19 September 2001 15:55:45 UTC