# Logic Clause

A Logic Clause is a Disjunction of Logic Literals.

**Context:**- It can range from being a Disjunctive Clause to being a Conjunctive Clause.
- a Horn Clause.

- It can be a part of a Logic Sentence.

- It can range from being a Disjunctive Clause to being a Conjunctive Clause.
**Example(s):****Counter-Example(s):****See:**Predicate Logic, Conjunctive Normal Form, Resolution Inference Rule.

## References

### 2012

- http://en.wikipedia.org/wiki/Clause_%28logic%29
- In logic, a
**clause**is a finite disjunction of literals.^{[1]}Clauses are usually written as follows, where the symbols [math]l_i[/math] are

- In logic, a

literals: :[math]l_1 \vee \cdots \vee l_n[/math] In some cases, clauses are written (or defined) as sets of literals, so that clause above would be written as [math]\{l_1, \ldots, l_n\}[/math]. 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 [math]\empty[/math], [math]\bot[/math], or [math]\Box[/math]. The truth evaluation of an empty clause is always [math]false[/math].

In first-order logic, a clause is interpreted as the universal closure of the disjunction of literals.^{[citation needed]} Formally, a first-order *atom* is a formula of the kind of [math]P(t_1,\ldots,t_n)[/math], where [math]P[/math] is a predicate of arity [math]n[/math] and each [math]t_i[/math] is an arbitrary term, possibly containing variables. A first-order *literal* is either an atom [math]P(t_1,\ldots,t_n)[/math] or a negated atom [math]\neg P(t_1,\ldots,t_n)[/math]. If [math]L_1,\ldots,L_m[/math] are literals, and [math]x_1,\ldots,x_k[/math] are their (free) variables, then [math]L_1,\ldots,L_m[/math] is a clause, implicitly read as the closed first-order formula [math]\forall x_1,\ldots,x_k . L_1,\ldots,L_m[/math]. 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 [math]b_1,\ldots,b_m[/math] are the literals in the body of a clause and [math]h_1,\ldots,h_n[/math] are those of its head, the clause is usually written as follows: :[math]h_1,\ldots,h_n \leftarrow b_1,\ldots,b_m[/math]

- 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'.*

*Symbolic Logic and Mechanical Theorem Proving*. Academic Press. p. 48. ISBN 0-12-170350-9.