A proof procedure is described which operates on formulas of the predicate calculus which are quantifier-free. The procedure, which involves a single inference rule called NC-resolution, is shown to be complete. Completeness is also obtained for a simple restriction on the rule’s application. Examples are given using NC-resolution not only for synthesis of a logic program from its specification, but for execution of a program specification in its original form.
Murray, Neil V., "A PROOF PROCEDURE FOR QUANTIFIER-FREE NON-CLAUSAL FIRST ORDER LOGIC" (1979). Electrical Engineering and Computer Science Technical Reports. Paper 39.