Clause (logic)

{{#invoke:Hatnote|hatnote}}

{{ safesubst:#invoke:Unsubst||$N=Confusing |date=__DATE__ |$B= {{#invoke:Message box|ambox}} }} In logic, a clause is a finite disjunction of literals. 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 $\emptyset$, $\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.{{ safesubst:#invoke:Unsubst||date=__DATE__ |$B= {{#invoke:Category handler|main}}{{#invoke:Category handler|main}} }} 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

• Conjunctive normal form
• Disjunctive normal form
• Horn clause

External links

• Clause logic related terminology
• Clause simultaneously translated in several languages and meanings