ETH Zuerich - Homepage
Information Security

Matthias Schmalz

Matthias Schmalz

ETH Zürich
Matthias Schmalz
CAB F 89
Universitaetstrasse 6
8092 Zürich

Phone: +41 44 632 72 50
Fax: +41 44 632 11 72


Diploma Thesis

Extensions of an Algorithm for Generalised Fair Model Checking


Isabelle for Event-B

The foundations are described in this technical report (theory files used for the technical report).

The tool is now available (installation instructions).


Currahee(E, iProver) is a theorem prover for TPTP problems with many irrelevant axioms. Currahee(E,iProver) applies a number of axiom selection strategies in parallel, and passes the resulting smaller problems to E and/or iProver. Currahee(E, iProver) version 0.1 has achieved the second rank in the LTB division of the CADE ATP systems competition of 2010.

Currahee uses the following axiom selection strategies:

Note that there are versions of E and iProver, namely E-LTB and iProver-SInE, that have been specially designed for problems with many irrelevant axioms. Currahee(E, iProver) uses the "ordinary" versions of E and iProver instead of E-LTB and iProver-SInE.




My PGP key


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 13 July 2011