COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > MaLARea: a Metasystem for Automated Reasoning in Large Theories

## MaLARea: a Metasystem for Automated Reasoning in Large TheoriesAdd to your list(s) Download to your calendar using vCal - Josef Urban (Charles University)
- Tuesday 22 January 2008, 13:00-14:00
- Computer Laboratory, William Gates Building, Room SS03.
If you have a question about this talk, please contact Thomas Tuerk. 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 (http://www.cs.miami.edu/~tptp/MPTPChallenge/) solving 142 problems out of 252, in comparison to E’s 89 and SPASS 81 solved problems. This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory Automated Reasoning Group Lunches
- Computer Laboratory talks
- Computer Laboratory, William Gates Building, Room SS03
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
Note that ex-directory lists are not shown. |
## Other listsKing's College Global Health Seminars Cambridge Geotechnical Society Seminar Series Cambridge Experimental and Behavioural Research Group (CEBEG)## Other talksReframing African Studies through Languages and Translation: Overcoming Barricades to Knowledge and Knowledge Management C++11/14 - the new C++ CANCELLED Jennifer Luff: Secrets, Lies, and the 'Special Relationship' in the Early Cold War Positive definite kernels for deterministic and stochastic approximations of (invariant) functions The quasi-stationary nature of ‘steady-state’ cyclic deformation Number, probability and community: the Duckworth-Lewis-Stern data model, Monte Carlo simulations and counterfactual futures in cricket |