Clause

A clause is a logical rule in a logic program. Formally, a clause is a disjunction of (possibly negated) literals, such as

$$grandfather(x,y) \vee \neg father(x,z) \vee \neg parent(z,y).$$

In the logic programming language Prolog this clause is written as

grandfather(X,Y) :- father(X,Z),

                           parent(Z,Y).

The part to the left of :- (“if”) is the head of the clause, and the right part is its body. Informally, the clause asserts the truth of the head given the truth of the body. A clause with exactly one literal in the head is called a Horn clause or definite clause; logic programs mostly consist of definite clauses. A clause without a body is also called a fact; a clause without a head is also called a denial, or a query in a proof by refutation. The clause without head or body is called the empty clause: it signifies inconsistency or falsehood and is denoted □ . Given a set of clauses, the resolution inference rule can be used to deduce logical consequences and answer queries (see First-Orde...