MaLARea swMATH ID: 10278 Software Authors: Urban, Josef Description: MaLARea: a Metasystem for Automated Reasoning in Large Theories. MaLARea (a Machine Learner for Automated Reasoning) is a simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS ATP systems) with a machine learning component (now the SNoW system used in the naive Bayesian learning mode). Its intended use is in large theories, i.e. on a large number of problems which in a consistent fashion use many axioms, lemmas, theorems, definitions and symbols. The system works in cycles of theorem proving followed by machine learning from successful proofs, using the learned information to prune the set of available axioms for the next theorem proving cycle. Although the metasystem is quite simple (ca. 1000 lines of Perl code), its design already now poses quite interesting questions about the nature of thinking, in particular, about how (and if and when) to combine learning from previous experience to attack difficult unsolved problems. The first version of MaLARea has been tested on the more difficult (chainy) division of the MPTP Challenge solving 142 problems out of 252, in comparison to E’s 89 and SPASS ’ 81 solved problems. It also outperforms the SRASS metasystem, which also uses E and SPASS as components, and solves 126 problems. Homepage: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.5291 Related Software: E Theorem Prover; Mizar; VAMPIRE; TPTP; MPTP 0.2; MaLeCoP; HOL Light; Flyspeck; MPTP; Metis_; BliStr; Isabelle/HOL; MaSh; MML; MoMM; OTTER; HOL; Sledgehammer; FEMaLeCoP; Coq Cited in: 49 Publications all top 5 Cited by 64 Authors 34 Urban, Josef 13 Kaliszyk, Cezary 10 Sutcliffe, Geoff 7 Kühlwein, Daniel 5 Vyskočil, Jiří 3 England, Matthew 3 Heskes, Tom M. 3 Jakubův, Jan 3 Tsivtsivadze, Evgeni 2 Alama, Jesse 2 Blanchette, Jasmin Christian 2 Florescu, Dorian 2 Gauthier, Thibault 2 Hoder, Kryštof 2 Paulson, Lawrence Charles 2 Pease, Adam 2 Schulz, Stephan 2 Voronkov, Andrei 2 Zombori, Zsolt 1 Armando, Alessandro 1 Bancerek, Grzegorz 1 Baumgartner, Peter 1 Bridge, James P. 1 Byliński, Czesław 1 Chvalovský, Karel 1 Cramer, Marcos 1 Csiszárik, Adrián 1 Dowek, Gilles 1 Färber, Michael 1 Furbach, Ulrich 1 Geuvers, Jan Herman 1 Grabowski, Adam 1 Greenaway, David 1 Heras, Jónathan 1 Höfner, Peter 1 Holden, Sean B. 1 Johansson, Moa 1 Koepke, Peter 1 Komendantskaya, Ekaterina 1 Korniłowicz, Artur 1 Korovin, Konstantin 1 Kumar, Ramana 1 López-Hernández, Julio César 1 Maclean, Ewen 1 Matuszewski, Roman 1 Michalewski, Henryk 1 Naumowicz, Adam 1 Norrish, Michael 1 Olšák, Miroslav 1 Pąk, Karol 1 Pelzer, Björn 1 Piotrowski, Bartosz 1 Pudlák, Pavel 1 Rawson, Michael 1 Reger, Giles 1 Rudnicki, Piotr 1 Schon, Claudia 1 Schröder, Bernhard 1 Siegel, Nick 1 Stanovský, David 1 Struth, Georg 1 Suda, Martin 1 Trac, Steven 1 van Laarhoven, Twan all top 5 Cited in 7 Serials 10 Journal of Automated Reasoning 2 AI Communications 2 Mathematics in Computer Science 1 Journal of Symbolic Computation 1 Annals of Mathematics and Artificial Intelligence 1 Lecture Notes in Computer Science 1 Journal of Formalized Reasoning Cited in 5 Fields 49 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 Numerical analysis (65-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year