Clause (logic)

In logic, a clause is a propositional formula formed from a finite collection of literals (atoms or their negations) and logical connectives.

A clause is true either whenever at least one of the literals that form it is true (a disjunctive clause, the most common use of the term), or when all of the literals that form it are true (a conjunctive clause, a less common use of the term).

That is, it is a finite disjunction[1] or conjunction of literals, depending on the context.

The truth evaluation of an empty disjunctive clause is always

The truth evaluation of an empty conjunctive clause is always

This is related to the concept of a vacuous truth.

Every nonempty (disjunctive) clause is logically equivalent to an implication of a head from a body, where the head is an arbitrary literal of the clause and the body is the conjunction of the complements of the other literals.

That is, if a truth assignment causes a clause to be true, and all of the literals of the body satisfy the clause, then the head must also be true.

This equivalence is commonly used in logic programming, where clauses are usually written as an implication in this form.

are those of its head, the clause is usually written as follows: This logic-related article is a stub.