E 3.0 Shangri-La(2023-11-15)
E 3.0 Shangri-La is the latest release of E. The main changes
compared to E 2.6 are support for full higher order logic and much
improved multicore-scheduling. This release is the cleaned up and
debugged version of both the 3.0 and 3.1 pre-release versions that
performed well in
CASC-J11 and
CASC-29 (with some
additional extra work).
E 2.6 Floral Guranse (2021-06-23)
E 2.6 Floral Guranse is the latest release of E. The main changes
over E 2.5 are full support for TFX, nearly full support for TH0
syntax (and some support for higher-order reasoning), more search
heuristics, some faster algorithms, and improved automatic modes.
- The README
file.
- What's new compared to version 2.5.
- The (draft) manual.
- The source distribution (~2464 kb)
- Various people kindly repackage E - I’ll link to these
downloads above if and when they become available.
E 2.5 Avongrove (2020-07-25)
E 2.5 Avongrove is the latest release of E. The main changes over
E 2.4 are stronger rewriting, better search heuristics, and
improved automatic modes.
- The README
file.
- What's new compared to version 2.4.
- The (draft) manual.
- The source distribution (~2412 kb)
- Various people kindly repackage E - I’ll link to these
downloads above if and when they become available.
E 2.4 Sandakphu (2019-10-23)
E 2.4
Sandakphu is the latest release of E. The main
changes are support for additional calculus variants, better
search heuristics, and much improved automatic modes.
- The README
file.
- What's new compared to version 2.3.
- The (draft) manual.
- The source distribution (~2270 kb)
- Various people kindly repackage E - I’ll link to these
downloads above if and when they become available.
E 2.3 Gielle (2019-03-12)
E 2.3
Gielle is the latest release of E. The main change
is the optional support for lambda-free higher-order logic. This
definite 2.3 release also features more robust clausification for
some large formulas of unusual structure.
- The README
file.
- What's new compared to version 2.2.
- The (draft) manual.
- The source distribution (~2170 kb)
- Various people kindly repackage E - I’ll link to these
downloads above if and when they become available.
E 2.2 Thurbo Moonlight (2018-10-23)
E 2.2
Thurbo Moonlight is the latest release of E. The
main changes are an internal reorganisation of orphan-handling and
proof objects, a much improved integration of PicoSAT, and
improvements in input validation and proof status reporting. As
usual, automatic modes are also improved.
- The README
file.
- What's new compared to version 2.1.
- The (draft) manual.
- The source distribution (~1951 kb)
- Various people kindly repackage E - I’ll link to these
downloads above if and when they become available.
E 2.1 Maharani Hills (2018-06-25)
E 2.1
Maharani Hills is the latest release of E. The main
changes are more robust implementation of certain TFF features and
an experimental integration of PicoSAT. Also, the internal
workflow for new clauses has been changed in a way that makes it
easier to batch-evaluate new clauses. As usual, automatic modes
are also improved.
E 2.0 Turzum (2017-07-04)
E 2.0
Turzum is the latest release of E. The main change
is support for many-sorted logic, i.e. support for the TPTP TFF
format (kindly contributed by Simon Cruanes), although currently
without interpreted arithmetic. Other changes include performance
improvements in clausification, better automatic modes, and proof
objects which keep input formula names intact.
E 1.9.1 Sungma (2016-08-31)
E 1.9.1
Sungma is the latest release of E. The main
user-visible changes are automatic format detection, improved
automatic modes, very much improved support for using the
watchlist to provide hints, and a bug-fix in clausification.
E 1.9 Sourenee (2015-07-14)
E 1.9
Sourenee is the latest release of E. The main
user-visible changes are better automatic modes and slightly more
compact proof objects, now also available for clausification and
in
Graphviz format for easy
visualisation.
E 1.8 Gopaldhara (2013-07-29)
E 1.8
Gopaldhara is the latest release of E. The main
user-visible changes are internal (and low-overhead) proof object
generation and an alternative automatic mode with strategy
scheduling.
E 1.7 Jun Chiabari(2013-03-24)
E 1.7
Jun Chiabari is the latest release of E. It
integrates condensing, various minor performance improvements, an
updated automatic mode and comes with a normalizer and interactive
query support via the LTB batch runner.
E 1.6 Tiger Hill(2012-07-10)
E 1.6
Tiger Hill is the latest release of E.It integrates
SInE-like preprocessing for large specifications, various minor
performance improvements, and has an updated and simplified
automatic mode.
E 1.5 Pussimbing(2012-05-05)
E 1.5
Pussimbing is the latest release of E. It features
significant speedups in the inference engine (in particular
superposition and subsumption), fixes various minor bugs, and has
an updated automatic mode.
E 1.4 Namring(2011-08-20)
E 1.4
Namring is the latest release of E. It features an
improved automatic mode, some more heuristic changes, fixing of
minor bugs, and general cleanup.
E 1.3 Ringtong (2011-06-27)
E 1.3
Ringtong is the latest release of E. It features an
improved automatic mode, adds answer substitution output, and
other minor improvements.
E 1.2 Badamtam (2010-09-24)
E 1.2
Badamtam is the latest release of E. It provides a
number of significant performance improvements.
Old archive
Versions of E older than E 1.2 are available from
the
old
archive page.
![[E logo]](IMAGES/eicon80.png)