The SETHEO System 
(system description)

by Ortrun Ibens 
Technische Universität München, Germany 

Abstract

SETHEO [LSBB92, GLMS94, MIL+97] is a theorem prover for first-order predicate logic. The SETHEO 
system includes an efficient inference machine with a preprocessing module for a specialized 
equality handling and a graphical proof display. Furthermore, Prolog-style built-ins are provided 
for logic-programming. The system is being continuously extended and enhanced with additional 
inference mechanisms and reduction techniques. The current version of SETHEO is V4.0.