||This article may be confusing or unclear to readers. (April 2010)|
In some cases, clauses are written (or defined) as sets of literals, so that clause above would be written as . That this set is to be interpreted as the disjunction of its elements is implied by the context. A clause can be empty; in this case, it is an empty set of literals. The empty clause is denoted by various symbols such as , , or . The truth evaluation of an empty clause is always .
In first-order logic, a clause is interpreted as the universal closure of the disjunction of literals. Formally, a first-order atom is a formula of the kind of , where is a predicate of arity and each is an arbitrary term, possibly containing variables. A first-order literal is either an atom or a negated atom . If are literals, and are their (free) variables, then is a clause, implicitly read as the closed first-order formula . The usual definition of satisfiability assumes free variables to be existentially quantified, so the omission of a quantifier is to be taken as a convention and not as a consequence of how the semantics deal with free variables.
In logic programming, clauses are usually written as the implication of a head from a body. In the simplest case, the body is a conjunction of literals while the head is a single literal. More generally, the head may be a disjunction of literals. If are the literals in the body of a clause and are those of its head, the clause is usually written as follows:
- If m=0 and n=1, the clause is called a (Prolog) fact.
- If m>0 and n=1, the clause is called a (Prolog) rule.
- If m>0 and n=0, the clause is called a (Prolog) query.
- If n>1, the clause is no longer Horn.