Accession Number : AD0717753

Title :   Some Linear Herbrand Proof Procedures: An Analysis,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Loveland,D. W.

Report Date : DEC 1970

Pagination or Media Count : 55

Abstract : Several Herbrand proof procedures proposed during the 1960 decade are shown to be related in varying degrees. Most of the paper deals with a relationship between s-linear resolution and model elimination. Refinements of each are proposed and the spaces of ground deductions are shown to be isomorphic in a suitable sense. The two refined procedures are then studied at the general level where they are no longer isomorphic and do not always relate to a natural ground level counterpart. Other topics considered are the introduction of an added merge condition to model elimination and also an expanded possible use of lemmas. Finally, the model elimination procedure is interpreted in the linked conjunct procedure of Davis and the matrix reduction procedure of Prawitz. (Author)

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

Subject Categories : Theoretical Mathematics
      Bionics

Distribution Statement : APPROVED FOR PUBLIC RELEASE