Can clause normal form include true/false constants?

194 Views Asked by At

As Wikipedia puts it,

... the only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable or a predicate symbol.

But first-order logic also includes constant symbols true and false. Is it accurate to say that, as these are not variables, they must be eliminated before a formula can be considered valid CNF?

1

There are 1 best solutions below

1
On

A clause is a disjunction of literals.

Thus, if we have $\bot$ in it, we can apply the equivalence $l \lor \bot \equiv l$ to cancel $\bot$.

But we you can also retain it; in conclusion we are trying to reach the "empty clause" that is exactly $\bot$.

If we end with two clauses $\lnot l$ and $l \lor \bot$ the resolution procedure will produce $\bot$, i.e. exactly $\square$, showing that the set of clauses is unsatisfiable.