Clause (logic)

From Wikipedia, the free encyclopedia
Jump to: navigation, search
For other uses, see Clause (disambiguation).

In logic, a clause is a finite disjunction of literals.[1] Clauses are usually written as follows, where the symbols l_i are literals:

l_1 \vee \cdots \vee l_n

In some cases, clauses are written (or defined) as sets of literals, so that clause above would be written as \{l_1, \ldots, l_n\}. 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 \empty, \bot, or \Box. The truth evaluation of an empty clause is always false.

In first-order logic, a clause is interpreted as the universal closure of the disjunction of literals.[citation needed] Formally, a first-order atom is a formula of the kind of P(t_1,\ldots,t_n), where P is a predicate of arity n and each t_i is an arbitrary term, possibly containing variables. A first-order literal is either an atom P(t_1,\ldots,t_n) or a negated atom \neg P(t_1,\ldots,t_n). If L_1,\ldots,L_m are literals, and x_1,\ldots,x_k are their (free) variables, then L_1,\ldots,L_m is a clause, implicitly read as the closed first-order formula \forall x_1,\ldots,x_k .
L_1,\ldots,L_m. 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 b_1,\ldots,b_m are the literals in the body of a clause and h_1,\ldots,h_n are those of its head, the clause is usually written as follows:

h_1,\ldots,h_n \leftarrow b_1,\ldots,b_m
  • If n=1 and m=0, the clause is called a (Prolog) fact.
  • If n=1 and m>0, the clause is called a (Prolog) rule.
  • If n=0 and m>0, the clause is called a (Prolog) query.
  • If n>1, the clause is no longer Horn.

See also[edit]


  1. ^ Chang, Chin-Liang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press. p. 48. ISBN 0-12-170350-9. 

External links[edit]