Clause (logic)

From formulasearchengine
Jump to navigation Jump to search


{{ 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


  1. {{#invoke:citation/CS1|citation |CitationClass=book }}

External links