Horn Clause

A Clause that has a conclusion of antecedents.

$$c\leftarrow h_1\wedge h_2\wedge \cdots \wedge h_n$$

Terminology

• $c$ : Goal, Head, Consequent
• $h_1$ : Subgoals, Tails, Antecedent
• Horn clause $c$ by itself: Fact
• Horn clause with only its tail $h_1\wedge \cdots \wedge h_n$: Resolution Rule

Undecidable Cases

There are no known solutions for defining rules for expression:

• $a_1\wedge \cdots \wedge a_3\to c_1\wedge c_2$
• $a_1\wedge \cdots \wedge a_3\to c_1\vee c_2$

Polarity

• Negative clause: comprised of only negative terms
  • $\neg S\wedge \neg T\to c$
• Positive clause: comprised of terms that can be positive
  • $S\wedge T\to c$
  • $(\neg S\vee T)\wedge (\neg Q\vee S)\to c$