Propositional Definite Clauses: The language of propositional definite clauses is a sublanguage of propositional calculus that does not allow uncertainty or ambiguity. In this language, propositions have the same meaning as in propositional calculus, but not all compound propositions are allowed in a knowledge base.
The syntax of propositional definite clauses is defined as follows:
Note that a definite clause is a restricted form of a clause. For example, the definite clause
a ← b ∧ c ∧ d.
is equivalent to the clause
a∨¬b∨¬c∨¬d.
In general, a definite clause is equivalent to a clause with exactly one positive literal (non-negated atom). Propositional definite clauses cannot represent disjunctions of atoms (e.g., a ∨ b) or disjunctions of negated atoms (e.g., ¬c∨¬d).