SETHEO: A high-performance theorem prover

A sound and complete theorem prover for first-order logic is presented, which is based on the connection method. The inference machine is implemented using PROLOG technology, an approach taken also with other systems, most prominently with Stickel's PTTP. But SETHEO differs from those in essential characteristics, among which are the following ones. It incorporates a powerful preprocessing module for a reduction of the input formula. The main proof procedure is realized as a variant of Warren's abstract machine.