RE: Rules are *not* Horn clauses!

From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>
Date: Wed, 19 Sep 2001 21:55:41 +0200
Message-ID: <511BB18E82E9D11188230008C724064602D9DDC6@tmex1.tm.tue.nl>
To: "'Pat Hayes'" <phayes@ai.uwf.edu>

```> >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

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:13 UTC