Concerning implementation, there exist two lines of development.
The older version (e.g. reference SETHEO V3.3 of January 1996) is implemented
as an interpreter for abstract machine code similar to the typical manner a
Prolog interpreter is realised. For this purpose, there exist two main
the compiler (inwasm) from logical notation to abstract machine code and the
interpreter (sam). This system was also intended to be used for
different extensions of the logic programming paradigm.
In the last years, the system has undergone a phase of complete redesign. After analysing the typical behaviour of the calculus on theorem proving applications, we have decided to give up the abstract machine paradigm and use a simpler and more modular architecture, which is also better suited for extensions of the calculus. High performance is achieved by a re-use technology (as described in the paper above). The current system is implemented in the scheme dialect bigloo. Although this implementation is much simpler and more robust concerning extensions, because of the employed re-use technology, the inference rates achieved on typical examples are even slightly higher than for the old implementation.
SETHEO is a project of the
About the older versions Setheo V3.2 and Setheo V3.0.
SETHEO V3.3 is available for the following platforms:
You get there the binaries compiled for the appropriate operating system together with a set of example problems. It should be useful to have a look at the README file
To obtain the sources of SETHEO contact us, we will make the access to the code possible then. If you could compile the programmes on your computer, please let us know that. If you had some problems, give us some information about, too. If you ported SETHEO to another platform, please mail us the changes you had to made.
Of course, we improve SETHEO between new releases, too. Patches, new scripts and related things can be obtained here in the patches directory of our ftp server.
SETHEO V3.3 can also be obtained via FTP as follows:
% ftp www8.informatik.tu-muenchen.de Name: anonymous Password: <your-e-mail-address> ftp> cd /pub/Automated_Reasoning/SETHEO ftp> binaryThen you can send a request for the file you want to get with one of the following commands.
ftp> get setheo.solaris.tar.gz ftp> get setheo.sunos.tar.gz ftp> get setheo.hp.tar.gz ftp> get setheo.linux.tar.gz ftp> get setheo.FreeBSD-2.2.tar.gz ftp> get READMEThen quit the ftp connection.
ftp> quitIf you have any further questions please contact
EMAIL: firstname.lastname@example.org SNAIL: Gernot Stenz Technische Universitüt München Lehrstuhl VIII für Informatik / AR D-80290 München Germany