Splitting and reduction heuristics in automatic theorem proving

摘要

A theorem proving program has been written in LISP which attempts to speed up automatic theorem proving by the use of heuristics. Some of these heuristics are of a general nature, applicable to the proof of any theorem in mathematics, while others are designed for set theory. Their effect is to break the theorem into parts which are easier to prove. The proof of these parts is then attempted by resolution. Resolution, when used, is relegated to the job it does best, proving relatively easy assertions.This program has been used to proe a large number of theorems in set theory, many of which would be impossible (because of time and storage restrictions) by current resolution methods.