Accession Number : AD0685613

Title :   REFINEMENT THEOREMS IN RESOLUTION THEORY,

Corporate Author : STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE

Personal Author(s) : Luckham,David

Report Date : 24 MAR 1969

Pagination or Media Count : 33

Abstract : The paper discusses some basic refinements of the Resolution Principle which are intended to improve the speed and efficiency of theorem-proving programs based on this rule of inference. It is proved that two of the refinements preserve the logical completeness of the proof procedure when used separately, but not when used in conjunction. The results of some preliminary experiments with the refinements are given. (Author)

Descriptors :   (*ARTIFICIAL INTELLIGENCE, *MATHEMATICAL LOGIC), LEARNING MACHINES, SET THEORY, THEOREMS

Subject Categories : Theoretical Mathematics
      Bionics

Distribution Statement : APPROVED FOR PUBLIC RELEASE