E.T. 0.2
J. Urban, J. Jakubuv, C. Kaliszyk, S. Schulz
Czech Technical University in Prague, University of Innsbruck, DHBW Stuttgart
Architecture
E.T. [KSUV15] 0.2 is a metasystem using E prover with specific strategies [Urb13,KU13,JU17] and
preprocessing tools [KUa13, KUb13, KUc13] that are targeted mainly at problems with many
redundant axioms. Its design is motivated by the recent experiments in
the Large-Theory Batch division [KUV14] and on the Flyspeck, Mizar and
Isabelle datasets, however, E.T. does no learning from related proofs.
Strategies
We characterize formulas by the symbols and terms that they contain,
normalized in various ways. Then we run various algorithms that try to
remove the redundant axioms and use special strategies on such
problems.
Implementation
The metasystem is implemented in ca. 1000 lines of Perl. It uses a
number of external programs, some of them based on E's code base, some
of them independently implemented in C++.
Expected Competition Performance
E.T. can solve some problems that E 1.8 cannot prove, and even some
TPTP problems with rating 1. The CASC performance should not be much
worse than that of E, possibly better, depending on problem selection.
References
- KSUV15
- Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jiri Vyskocil (2015),
System Description: E.T. 0.1.,
CADE 2015: 389-398
- Urb13
- Urban J. (2013),
BliStr: The Blind Strategymaker.,
CoRR abs/1301.2683 (2013)
- KU13
- Kaliszyk C., Urban J. (2013)
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution,
In Blanchette J.C., Urban J.,
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 87-95
(Lake Placid, USA),
EasyChair Proceedings in Computing.
- KUa13
- Kaliszyk C., Urban J. (2013),
MizAR 40 for Mizar 40,
CoRR abs/1310.2805 (2013)
- JU17
- Jan Jakubuv, Josef Urban (2017),
BliStrTune: hierarchical invention of theorem proving strategies,
CPP 2017: 43-52
- KUb13
- Kaliszyk C., Urban J. (2013),
Automated reasoning service for HOL Light,
Intelligent Computer Mathematics, 120-135
- KUV14
- Kaliszyk C., Urban J., Vyskocil J. (2014),
Machine Learner for Automated Reasoning 0.4 and 0.5,
CoRR abs/1402.2359 (2014)
- KUc13
- Kaliszyk C., Urban J., (2013),
Lemma Mining over HOL Light,
Logic for Programming, Artificial Intelligence, and Reasoning, 503-517