MPI-INF Logo
Campus Event Calendar

Event Entry

New for: D1, D2, D3, D4, D5

What and Who

The Inside and Outside of E

Schulz, Stephan
TU München, FB Informatik
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS  
AG Audience

Date, Time and Location

Wednesday, 13 December 2006
14:00
-- Not specified --
E1 4
Rotunde 6.OG
Saarbrücken

Abstract

E is a modern, high-performance theorem prover for full first-order logic with equality. It is based on the superposition calculus with a

number of extensions both for preprocessing and for the proof search proper. While the implementation borrows many proven techniques
from older implementations, E has also pioneered novel approaches, particularly in data representation, indexing, and search control.
However, while E is rather unique on the inside, it very much tries to conform to (or set) standards on the outside.
E is implemented in ANSI/ISO C and uses (a minimal subset) of the POSIX specification for additional operating system services.
As a consequence, it is widely portable and easy to install on nearly any modern UNIX-like operating system, and even on
Windows (using CygWin). E itself can read and write data in the LOP/PCL, TPTP-2 and TPTP-3 formats. It also uses the SZS
output ontology to describe the result of the proof search. As a consequence, it plays well with other systems and has been integrated
into several larger systems.

Contact

Roxane Wetzel
9325-900
--email hidden
passcode not visible
logged in users only

Roxane Wetzel, 12/13/2006 14:51
Roxane Wetzel, 12/13/2006 14:49 -- Created document.