Propositional Definite Clauses

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:

• An atomic proposition or atom is the same as in propositional calculus.
• A body is an atom or a conjunction of atoms. Defined recursively, a body is either an atom or of the form a ∧ b, where a is an atom and b is a body.
• A definite clause is either an atom a, called an atomic clause, or of the form
• a ← b, called a rule, where a, the head, is an atom and b is a body.
• A knowledge base is a set of definite clauses.

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