Document Type
Report
Date
2-1979
Keywords
logic
Language
English
Disciplines
Computer Sciences
Description/Abstract
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.
Recommended Citation
Murray, Neil V., "A PROOF PROCEDURE FOR QUANTIFIER-FREE NON-CLAUSAL FIRST ORDER LOGIC" (1979). Electrical Engineering and Computer Science - Technical Reports. 39.
https://surface.syr.edu/eecs_techreports/39
Source
local
