E: Questions and Answers

What is the difference between E and a PROLOG system?

Here is a list of the most important differences:

• Advantages of PROLOG:
  • You can write procedural code with semi-explicit control flow and cuts.
  • PROLOG has a pretty rich set of predefined predicates, i.e. numbers, arithmetic, I/O-Statements and so on.
  • PROLOG is a mature technology, and may be faster for some classes of probems.
• Advantages of E:
  • E has purely declarative semantics: a<-b. is fully equivalent to a;~b. is fully equivalent to ~b;a. is fully equivalent to ~b<-~a. While E allows procedural clauses (as in a:-b.), that is only for compatibility with SETHEO. Procedural clauses are treated exactly as declarative ones. The most natural clause representation for E is probably a literal disjunction: a=$true;b!=$true;c!=$true.
  • E has a richer language, not restricted to Horn clauses (i.e. we can write a;b <- c,d., meaning "if c and d then a or b"). You can use explicitly negated atoms, as in ~a <- b. (In fact, starting with E 0.82, E supports full first order format in TPTP and TSTP syntax, for a much richer input language).
  • E has basically no predefined predicates and function symbols. You want it - you specify it. No relying on cheesy machine arithmetic ;-)
  • E is complete. If the query follows from the axioms, E will find a proof (well, theoretically - in practice the computer or the user may run out of resources or patience) unless the user explicitly selects an incomplete search strategy.
  • E has a different (stronger) concept of equality on terms, not modulo unification, but modulo an equational first-order theory (which is part of the input problem).
  • Due to clever search strategies, E may be faster for some classes of problems.

What happened to the snapshot releases?

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

CLIB? Why the hell is it called CLIB?

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

So what does the funny nickname mean?

• Risheehat is the name of a tea garden in Darjeeling making one of the worlds finest first flush Darjeeling teas.
• Yunnan is a region in China producing a famous black tea with a redish tint.
• Castleton is a very small tea garden in Darjeeling making an excellent second flush Darjeeling tea.
• Jungpana is a tea garden in Darjeeling making a very good and quite famous second flush Darjeeling tea.
• Lingia is a tea garden making a very good first flush Darjeeling tea. It's nearly as good as the Risheehat (in my opinion), but more expensive.
• Phuguri is a decent first flush Darjeeling I tried during the work on E 0.5.
• Mim is a very fine first flush Darjeeling that, surprisingly enough, can stand hard water fairly well, and which I hence tend to drink a lot while travelling.
• Kanchanjangha is an ecologically produced tea from Nepal. I quite like Nepalese tea, and tried to find a new variety. It is not bad, but not up to the Darjeelings I am used to (yes, I am a tea snob).
• North Tukvar is a somewhat bigger tea garden in Darjeeling. Their claim to fame is that they managed to bring the first tea of the 2001 harvesting period into my tea shop.
• Mullotar is a fairly large tea garden producing a quite nice organically grown first flush that offers excellent value for money (if you buy a kilogramm at a time ;-)
• Nuwara Eliya is one of the very best Ceylon (now Sri Lanka) highland teas.
• Dhajea is a tea garden making a very good (not quite great) first flush Darjeeling tea.
• Puttabong is another Darjeeling tea garden which provided me with a very good new harvest first flush in 2003.
• Steinthal is a small, but quite old and famous Darjeeling tea garden, with particularly good second flush teas.
• Tumsong is a medium sized garden in Eastern Darjeeling.
• Lung Ching or Dragon's Well Tea is a famous (and quite good) gree tea from the Zhejiang province in mainland China.
• Soom is a tea garden in Darjeeling supplying me with a lot of new early harvest tea in 2005.
• Kanyam is a tea garden in Nepal. I am impressed - I found that a 2005 first flush Kanyam was comparable to my rather good Darjeelings!
• Singtom is a Darjeeling tea garden.
• Longview is another Darjeeling tea garden providing an excellent 2007 first flush.
• Temi is a very good tea from Sikkim on the Southern slopes of the Himalaya.
• Balasun is the tea estate in the Eastern Himalaya that provided me with a very nice 2009 early harvest Darjeeling.

Are there more people doing strange stuff like this?

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

• SETHEO is a top-down model-elemination prover. It's fate is to be mated to E and thus to form a composite prover. This shows particularly in the fact that E's native input syntax is a dialect of LOP as used by SETHEO.
• DISCOUNT and Waldmeister are two provers for unit-equational problems. Experiences with DISCOUNT have had a profound effect on many design decisions for E, in particular on the way search heuristics are specified. The extremely impressive results of Waldmeister made me choose perfect discrimination trees as the main indexing structure in E.
• SPASS is the first high performance theorem prover based on superposition I became aware of. I use it as a benchmarking tool and for debugging ("If it's easy for SPASS it should be easy for E").
• Finally, Otter (or, more exactly, discussions with it's main author, Bill McCune) also gave me some ideas now incorporated into E. Bill has a new system, Prover 9, that borrows from E in return.
• Vampire is another high-performance theorem prover. E and Vampire are about as far from each other as two high-performance saturationg provers can be. However, there is a useful exchange of ideas.