SETHEO: A high-performance theorem prover (Q1189726)

The paper deals with a theoretical background and practical knowledge of the implementation of the interesting system SETHEO --- a theorem prover for first order logic. The system is based on the connection method and is proved to be sound and complete. SETHEO can be used as an interpreter for the programming language LOP (under development). The inference machine of the system is implemented using Prolog technology, but there are some special characteristics differing SETHEO from common Prolog systems: a powerful preprocessing module for a reduction of the input formula, the proof procedure is realized as a WAM, factorization, lemma generation and the application of proof schemata are offered as options. The entire system is implemented in the language \(C\) and is running on several machines. The important feature of SETHEO is its performance of up to 70 Klips on a SUN SPARC station 1 with 12 Mips.