CLAUSE (LOGIC)

In logic, a 'clause' is a disjunction of
literals. In propositional logic, clauses
are usually written as follows, where the symbols $l\_i$ are
literals:
:
In some cases, clauses are written 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 then hinted from 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$,
, or $Box$. The truth evaluation of an empty
clause is always $false$.
In first-order logic, a clause is the universal quantification of all free
variables of a quantifier-free disjunction of literals. Formally, a first-order
literal is 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. 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. First-order clauses are sometimes written
omitting the quantifiers, so that the above clause is written
$L\_1,ldots,L\_m$. This omission is justified by the fact that, for
being a clause, a disjunction of literals must have all variables universally
quantified. In case a clause is valid or checked for validity, this universal
quantification is also implicit in the semantics. However, the definition of satisfiability assumes free variables to be existentially quantified, so the omission of 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 simpest 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$ those of its head, the clause
is usually written:
:$h\_1,ldots,h\_n\; :-\; b\_1,ldots,b\_m$
In computer programming, a clause is a series of statements executed upon the evaluation of a conditional expression. A condition may not always be explicitly applied to a clause; these are usually called ''non-conditional'', ''main'', or ''functional'' clauses. A clause may also be referenced by the structure of the conditional expression, for example ''I am inserting a case-clause where $type is equal to 'auto'.'' ''Modifications are necessary to the if-then clause where the ninth subscript of $array ($array[9]) is equal to 'Sam'.''

Contents

See also

See also

★ Conjunctive normal form

★ Horn clause

★ Clause logic related terminolgy