Some theorem-proving strategies and their implementation. [Instructions for using PG1 (in COMPASS for CDC 3600)]
George A. Robinson, L. Wos, Daniel F. Carson · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 1964
First, the paper discusses the idea of proof and resolution as generalized syllogism. Some early computer-oriented theorem-proving efforts are sketched, and then the paper concentrates on one particular strategy of search, the unit preference strategy. This strategy has been implemented in a theorem-proving program now successfully running on a CDC 3600. The paper describes the search algorithm employed in the program, proves its soundness and completeness, considers some examples, and describes additional search strategies that can be employed to effect further improvement. The following aspects of the computer code PG1 (coded in COMPASS) are explained: input, output, arrangement of data in memory, algorithms, deletion strategies, restart information, and proof recovery. Three appendixes present pertinent concepts and notation from predicate calculus, additional concepts and notations related to resolution, and some proofs produced by PG1. (RWR)