E 1.0x

User Manual

–preliminary version–

Stephan Schulz

September 16, 2011

Abstract

E is an equational theorem prover for full clausal logic, based on superposition and rewriting. In this very preliminary manual we first give a short introduction for impatient new users, and then cover calculus, control, options and input/output of the prover in some more detail.

Contents
1 Introduction
2 Getting Started
3 Calculus and Proof Procedure
 3.1 Calculus
 3.2 Proof Procedure
4 Usage
 4.1 Search Control Heuristics
 4.2 Term Orderings
 4.3 Literal Selection Strategies
 4.4 The Watchlist Feature
 4.5 Learning Clause Evaluation Functions
 4.6 Other Options
5 Input Language
 5.1 LOP
 5.2 TPTP Format
6 Output…or how to interpret what you see
 6.1 The Bare Essentials
 6.2 Impressing your Friends
 6.3 Detailed Reporting
 6.4 Requesting Specific Results
A License
References