Download Introduction to Prolog Programming

Ulle Endriss. And Introduction to Prolog Programming
63
(2) Commas separating subgoals correspond to conjunctions in logic (i.e., you have to
replace every comma between two predicates by a ∧ in the formula).
(3) Prolog rules are mapped to implications, where the rule body is the antecedent and
the rule head the consequent (i.e., rewrite :- as → and change the order of head
and body).
(4) Queries are mapped to implications, where the body of the query is the antecedent
and the consequent is ⊥ (i.e., rewrite :- or ?- as →, which is put after the translation of the body and followed by ⊥).
(5) Each variable occurring in a clause has to be universally quantified in the formula
(i.e., write ∀x in front of the whole formula for each variable X).
6.2
Horn Formulas and Resolution
The formulas we get when translating Prolog rules all have a similar structure: they
are implications with an atom in the consequent and a conjunction of atoms in the
antecedent (this implication again is usually in the scope of a sequence of universal
quantifiers). Abstracting from the quantification for the moment, these formulas all
have the following structure:
A1 ∧ A2 ∧ · · · ∧ An → B
Such a formula can be rewritten as follows:
A1 ∧ A2 ∧ · · · ∧ An → B
≡
¬(A1 ∧ A2 ∧ · · · ∧ An ) ∨ B ≡
¬A1 ∨ ¬A2 ∨ · · · ∨ ¬An ∨ B
Note that if B is ⊥ (which is the case when we translate queries) we obtain the following:
¬A1 ∨ ¬A2 ∨ · · · ∨ ¬An ∨ ⊥ ≡ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬An
Hence, every formula we get when translating a Prolog program into first-order formulas
can be transformed into a universally quantified disjunction of literals with at most one
positive literal. Such formulas are called Horn formulas.1 (Sometimes the term Horn
formula is also used to refer to conjunctions of disjunctions of literals with at most one
positive literal each; that would corresponds to an entire Prolog program.)
As A→⊥ is logically equivalent to ¬A, by translating queries as implications with ⊥ in
the consequent we are basically putting the negation of the goal in a query into the set of
formulas. Answering a query in Prolog means showing that the set corresponding to the
associated program together with the translation of that query is logically inconsistent.
1
A Prolog fact is simply translated into an atomic formula, i.e., a positive literal. Therefore, formulas
representing facts are also Horn formulas.