Technische Universität München,
Fakultät für Informatik
Lehrstuhl Informatik IV,
Research Group Automated Reasoning
E and E-SETHEO -- Trophies
The CASC theorem
proving competition has been held annually since 1996. It compares the
performance of sound, fully automatic, classical 1st order ATP
systems. Various versions of our provers have successfully
participated since the very first CASC, held at CADE-13 in 1996).
After several years of good showing accros the board, E was recognized
as the "overall best" prover in the 2010 CASC-J5. It came in second in
FOF and third (after two version of Vampire) in CNF, 4th in UEQ, 5th
in FNT, and participated successfully in LTB and EPR.
From left to right: FOF, MIX assurance, EPR
The FOF division
The FOF division compared the performance of theorem provers on
theorems spcified in full first-order format. In 2001, it was won by
E-SETHEO, which beat last year's winner Vampire.
The MIX division
E-SETHEO and Vampire
shared the win in the MIX division assurance class. In this division,
theorems are specified as (unsatisfiable) problems in clause normal
form. Provers only have to find a proof, they do not need to present a
proof object. This year, the first 6 places in a field of 11 were
taken by different versions of E-SETHEO, E, and Vampire. In the proof
classs, where provers have to generate an explicit proof object, E won
3rd place after two versions of Vampire.
The EPR division
In EPR, provers have to determine the status (satisfiable or
unsatisfiable) of near-propositional problems specifies in clause
normal form. This category was won by E-SETHEO. The runner-up, PizEAndSato,
is also based on E's library (and SATO).
Other successes
In the UEQ division (unit-equational problems), E won a very good
third place after two versions of Waldmeister. Similarly,
in the SAT division, E-SETHO achieved a third place after two versions
of Gandalf
optimized for model finding.
From left to right: MIX and SEM
The MIX division
In 2000, E managed to beat E-SETHEO by a hair's breadth (well, by an
average of 80 seconds per problem...) to snatch the trophy for the MIX
division. E was particularly strong on Horn problems, winning both the
HEQ and the HNE subdivisions, as well as PEQ (purely equational
non-unit problems).
The SEM division
The SEM division, first-order probems from a single semantic domain
(SET theory) was won by E-SETHEO.
Other successes
E-SETHEO achieved a third place in the FOF division in 2000. It did
not enter the SAT division.
Stephan
Schulz,schulz@informatik.tu-muenchen.de, 20.8.2001