# 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.[1] Clauses are usually written as follows, where the symbols ${\displaystyle l_{i}}$ are literals:

${\displaystyle 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 ${\displaystyle \{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 ${\displaystyle \emptyset }$, ${\displaystyle \bot }$, or ${\displaystyle \Box }$. The truth evaluation of an empty clause is always ${\displaystyle 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}}[citation needed] }} Formally, a first-order atom is a formula of the kind of ${\displaystyle P(t_{1},\ldots ,t_{n})}$, where ${\displaystyle P}$ is a predicate of arity ${\displaystyle n}$ and each ${\displaystyle t_{i}}$ is an arbitrary term, possibly containing variables. A first-order literal is either an atom ${\displaystyle P(t_{1},\ldots ,t_{n})}$ or a negated atom ${\displaystyle \neg P(t_{1},\ldots ,t_{n})}$. If ${\displaystyle L_{1},\ldots ,L_{m}}$ are literals, and ${\displaystyle x_{1},\ldots ,x_{k}}$ are their (free) variables, then ${\displaystyle L_{1},\ldots ,L_{m}}$ is a clause, implicitly read as the closed first-order formula ${\displaystyle \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 ${\displaystyle b_{1},\ldots ,b_{m}}$ are the literals in the body of a clause and ${\displaystyle h_{1},\ldots ,h_{n}}$ are those of its head, the clause is usually written as follows:

${\displaystyle 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.