A non-clausal theorem proving system
David E. Wilkins · Artificial Intelligence and the Simulation of Behaviour · 1974
There are reasons to suspect that non-clausal first-order logic expressions will provide a better base for a theorem prover than conventional clausal form. A complete inference system, QUEST, for the first-order predicate calculus using expressions in prenex form is presented. Comparison of this system with SL-resolution shows that clausal techniques can be transferred to prenex form and expected advantages do seem to appear.