MaLARea 0.4

J. Urban, D. Kuehlwein, S. Schulz, J. Vyskocil
Radboud University Nijmegen, TU Munchen, Czech Technical University

Architecture

MaLARea 0.4 [Urb07, USPV08] is a metasystem for ATP in large theories where symbol and formula names are used consistently. It uses several deductive systems (now E,SPASS,Vampire, Paradox, Mace), as well as complementary AI techniques like machine learning (the SNoW system) based on symbol-based similarity, model-based similarity, term-based similarity, and obviously previous successful proofs. The version for CASC 2012 will mainly use E prover, possibly also Prover9, Mace and Paradox. The premise selection methods will likely also use kernel-based learning and E's implementation of SInE.

Strategies

The basic strategy is to run ATPs on problems, then use the machine learner to learn axiom relevance for conjectures from solutions, and use the most relevant axioms for next ATP attempts. This is iterated, using different timelimits and axiom limits. Various features are used for learning, and the learning is complemented by other criteria like model-based reasoning, symbol and term-based similarity, etc.

Implementation

The metasystem is implemented in ca. 2500 lines of Perl. It uses many external programs - the above mentioned ATPs and machine learner, TPTP utilities, LADR utilities for work with models, and some standard Unix tools. MaLARea is available at 
    https://github.com/JUrban/MPTP2/tree/master/MaLARea
The metasystem's Perl code is released under GPL2.

Expected Competition Performance

Thanks to machine learning, MaLARea is strongest on batches of many related problems with many redundant axioms where some of the problems are easy to solve and can be used for learning the axiom relevance. MaLARea is not very good when all problems are too difficult (nothing to learn from), or the problems (are few and) have nothing in common. Some of its techniques (selection by symbol and term-based similarity, model-based reasoning) could however make it even there slightly stronger than standard ATPs. MaLARea has a very good performance on the MPTP Challenge, which is a predecessor of the LTB division, and it is the winner of the 2008 MZR LTB category which had the same rules as the MPTP Challenge. Since then the LTB rules changed and MaLARea did not compete.

References

Urb07
Urban J. (2007), MaLARea: a Metasystem for Automated Reasoning in Large Theories., In Sutcliffe G., Urban J., Schulz S., Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (Bremen, Germany), CEUR Workshop Proceedings,.
USPV08
Urban J., Sutcliffe G., Pudlak P., Vyskocil J. (2007), MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance, In Baumgartner P., Armando A., Gilles D., Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia), Lecture Notes in Artificial Intelligence (To appear).