Clause (logic)
From ArticleWorld
In logic programming, a clause refers to a disjunction of literals, which may be either positive or negative.
[edit]
Related terminology
- Statement: A statement is a declarative sentence that can be assigned one and only one of the two possible truth values, true or false. In other words, a statement is a sentence that affirms or denies something and is either true or false.
- Connective: A connective or logical connective is a syntactic operation on statements, or the symbol for such an operation, which corresponds to a logical operation on the logical values of those statements. The basic connectives are “NOT” (~), “AND” (^), “OR” (v), “conditional” or “if-then” (→), and “biconditional” or “if-and-only-if” (iff) (↔).
- Literal: If ‘p’ is a propositional symbol (i.e. a symbol denoting a statement), then p and ~p (negation of p) are literals. In other words, a literal refers to a statement that does not have any connectives other than NOT (~).
- Disjunction: A disjunction refers to the logical OR operation. It contrasts with conjunction, which refers to the logical AND operation.
- Clause: A clause is a disjunction of literals. If l--1, l2, …, ln are literals, then the clause can be written as: l--1v l2 v … v ln.
- Conjunctive normal form: A statement is said to be in conjunctive normal form (CNF) if it consists of a single clause or a conjunction of clauses. Such a statement is also referred to as a clause set.
[edit]
Types of clause
- Unit clause: A unit clause is a clause consisting of a single literal.
- Positive clause, negative clause, empty clause and mixed clause: A clause that has no negative literals is a positive clause and a clause that has no positive literals is a negative clause. An empty clause or a null clause has zero positive and zero negative literals. A mixed clause has at least one positive and at least one negative literal.
- Horn clause: A Horn clause is a clause with at most one positive literal. A set of Horn clauses makes a Horn set.
- Definite clause: A definite clause is a Horn clause that has exactly one positive literal.