# 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 are
literals:

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

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 , where
is a predicate of arity and each
is an arbitrary term, possibly containing variables. A first-order *literal* is either an atom or a negated atom . If
are literals, and are
their (free) variables, then is a clause, implicitly read as the closed first-order formula .
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 are the literals in the body of a clause and are those of its head, the clause is usually written as follows:

- 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

## References

- ↑ {{#invoke:citation/CS1|citation |CitationClass=book }}