Gilmore's program used conversion to disjunctive normal form, a form in which the satisfiability of a formula is obvious.

Decidability of the problem

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the common case of propositional logic, the problem is decidable but co-NP-complete, and hence only exponential-time

1.Previous
3.Next