A PROOF PROCEDURE FOR QUANTIFIER-FREE NON-CLAUSAL FIRST ORDER LOGIC

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