| Description: |
A clause is a disjunction of literals, where usually unbound variables
are meant to be all-quantified.
Example:
P(g(X, e), f(c, Y)) ∨ P(g(Y), c) ∨ ¬
Q(f(X, Y)) ∨ ¬ P(d, f(X, e)), with
- P and Q predicate symbols,
- f and g function symbols,
- X and Y variables, and
- c, d ,e constants.
Clauses can be written in implication form. The clause above can
be rewritten as:
- P(g(X, e), f(c, Y)) ∨ P(g(Y), c) ←
Q(f(X, Y), d) ∧ P(d, f(X, e)), or, with explicit
quantifiers, as
- (∀X)(∀Y) [ P(g(X, e), f(c, Y)) ∨
P(g(Y), c) ← Q(f(X, Y), d) ∧ P(d, f(X, e)) ].
|
