Technische Universität München, Fakultät für Informatik
Lehrstuhl Informatik IV, Research Group Automated Reasoning

E: Questions and Answers

What is the difference between E and a PROLOG system?

To put it short, E is a theorem prover and PROLOG is a programming language. Although they both can solve a common subset of problems, there are some significant differences. E works in a bottom-up fashion, systematically generating consequences from the set of input clauses, until a contradictiom (i.e. a proof) has been found. PROLOG uses SLD resolution to find a solution in a top-down depth-first fashion, and, consequently, is not complete, i.e. it can run forever although a solution exists.

Here is a list of the most important differences:

You can try to get E and feed some simple PROLOG code into it to see what happens (simple means "no numbers, no predefined predicates"). As far as I know, the LOP syntax of E is a superset of basic PROLOG without numbers and predefined symbols (but I am not very much into PROLOG).

What happened to the snapshot releases?

I'm now doing a lot of development work off-line on my laptop. As one consequence, the snapshot was only updated very infrequently. As few people used it, I just decided to discontinue it. Email me for the latest version (you get the added benefit of a defined state ;-).

Is it just me or is the distribution getting smaller and smaller?

Not any longer. It did for some time, but finally feature creep has caught up with this mysterious effect. I did not have a good explanation for the effect while it lasted. While I am always trying to cut some old cruft here and there, I also keep adding new features. Some of the effect may be due to random amounts of backup files or profiling data in the directories. All in all, I just put it down as a strange and interesting effect.

CLIB? Why the hell is it called CLIB?

Because C++ sucks big rocks through small straws like nothing short of a pack of giant vampire squids. Yes, really, that's the reason ;-)

Moreover, the latest versions are not called CLIB anymore, but just E.

So what does the funny nickname mean?

Starting with E 0.22, each release version has received a nickname. This usually is the name of a tea (or the corresponding tea garden) which I drank a lot while programming the version.

Are there more people doing strange stuff like this?

Yes, a couple of groups do work on theorem proving. The people at the Argonne National Laboratories have a fairly complete list. There also is an introduction to automated reasoning on the web, which has another list of systems.

There are a couple of theorem provers that had not insignificant influence on the design of E:

Stephan Schulz,, 5.7.2000