Document Type

Report

Date

2-1979

Embargo Period

4-25-2012

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.

Source

local

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.