Intellectics Group: Technical Report 97-01
On the Advantage of a Non-Clausal
We propose a non-clausal decision procedure for classical propositional
logic. It is a generalization of the Davis-Putnam procedure and deals with
formulae which are not necessarily in clausal form. Since there is no need to
translate the investigated formula into normal form, we avoid increasing its
size but preserve its structure. This will in general lead
to a much smaller search space and thus to a more efficient method.
We introduce a short Prolog implementation of our procedure showing that
it is possible to implement a non-clausal decision procedure in a compact and
adaptable way. To demonstrate the good performance of the non-clausal approach
some experimental results are provided. To this end we compare the non-clausal
implementation with a clausal-based Davis-Putnam prover using the standard
translation into clausal form as well as the definitional translation.