Clause (logic)

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

In logic, a clause is an expression formed from a finite collection of literals (variables or their negations) that is true whenever at least one of the literals that form it is true. That is, it 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

Empty clauses[edit]

A clause can be empty (defined from 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.

Implicative form[edit]

Every nonempty clause is logically equivalent to an implication of a head from a body, where the head is an arbitrary literal of the clause and the body is the conjunction of the negations of the other literals. That is, if a truth assignment causes a clause to be true and none of the literals of the body satisfy the clause, then the head must also be true.

This equivalence is comminly used in logic programming, where clauses are usually written as an implication in this form. 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]

References[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]