Logic Clause

From GM-RKB
Jump to navigation Jump to search

A Logic Clause is a Disjunction of Logic Literals.



References

2012

literals: :[math]\displaystyle{ 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]\displaystyle{ \{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]\displaystyle{ \empty }[/math], [math]\displaystyle{ \bot }[/math], or [math]\displaystyle{ \Box }[/math]. The truth evaluation of an empty clause is always [math]\displaystyle{ 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]\displaystyle{ P(t_1,\ldots,t_n) }[/math], where [math]\displaystyle{ P }[/math] is a predicate of arity [math]\displaystyle{ n }[/math] and each [math]\displaystyle{ t_i }[/math] is an arbitrary term, possibly containing variables. A first-order literal is either an atom [math]\displaystyle{ P(t_1,\ldots,t_n) }[/math] or a negated atom [math]\displaystyle{ \neg P(t_1,\ldots,t_n) }[/math]. If [math]\displaystyle{ L_1,\ldots,L_m }[/math] are literals, and [math]\displaystyle{ x_1,\ldots,x_k }[/math] are their (free) variables, then [math]\displaystyle{ L_1,\ldots,L_m }[/math] is a clause, implicitly read as the closed first-order formula [math]\displaystyle{ \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]\displaystyle{ b_1,\ldots,b_m }[/math] are the literals in the body of a clause and [math]\displaystyle{ h_1,\ldots,h_n }[/math] are those of its head, the clause is usually written as follows: :[math]\displaystyle{ h_1,\ldots,h_n \leftarrow b_1,\ldots,b_m }[/math]

    • 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'.
  1. Chang, Chin-Liang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press. p. 48. ISBN 0-12-170350-9.