Clause (logic)

In logic, a clause is a finite disjunction of literals.[1] Clauses are usually written as follows, where the symbols li 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 \empty, \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.[citation needed] 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 ti 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 m=0 and n=1, the clause is called a (Prolog) fact.
  • If m>0 and n=1, the clause is called a (Prolog) rule.
  • If m>0 and n=0, the clause is called a (Prolog) query.
  • If n>1, the clause is no longer Horn.

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

See also

References

  1. ^ Chang, Chin-Liang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press. p. 48. ISBN 0121703509. 

External links


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Clause (disambiguation) — Clause may refer to: Clause, a grammatical construct; Clause (logic), a disjunction of literals in logic; Frederick Clause, surgeon, painter and early explorer of Western Australia. An individually designated provision in a contract, regulation… …   Wikipedia

  • Logic programming — is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy s [1958] advice taker proposal, logic is used as a purely declarative… …   Wikipedia

  • Clause De Horn — Pour les articles homonymes, voir Horn. La dénomination « clause de Horn » vient du nom du logicien Alfred Horn qui, le premier, met en évidence l’intérêt de telles clauses en 1951 dans l’article « On sentences which are true of… …   Wikipédia en Français

  • logic — logicless, adj. /loj ik/, n. 1. the science that investigates the principles governing correct or reliable inference. 2. a particular method of reasoning or argumentation: We were unable to follow his logic. 3. the system or principles of… …   Universalium

  • Clause de Horn — Pour les articles homonymes, voir Horn. En logique, en particulier en calcul propositionnel, une clause de Horn est une clause comportant au plus un littéral positif. Il existe donc trois types de clauses de Horn : celles qui comportent un… …   Wikipédia en Français

  • Horn clause — In mathematical logic, a Horn clause is a clause (a disjunction of literals) with at most one positive literal. They are named after the logician Alfred Horn, who first pointed out the significance of such clauses in 1951. Horn clauses play a… …   Wikipedia

  • Outline of logic — The following outline is provided as an overview of and topical guide to logic: Logic – formal science of using reason, considered a branch of both philosophy and mathematics. Logic investigates and classifies the structure of statements and… …   Wikipedia

  • Algebraic Logic Functional programming language — also known as ALF is a programming language which combines functional and logic programming techniques. Its foundation is Horn clause logic with equality which consists of predicates and Horn clauses for logic programming, and functions and… …   Wikipedia

  • Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

  • Constraint logic programming — Programming paradigms Agent oriented Automata based Component based Flow based Pipelined Concatenative Concurrent computing …   Wikipedia


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.