BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:MaLARea: a Metasystem for Automated Reasoning in Large Theories - 
 Josef Urban (Charles University)
DTSTART:20080122T130000Z
DTEND:20080122T140000Z
UID:TALK9881@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:MaLARea (a Machine Learner for Automated Reasoning) is a simpl
 e metasystem iteratively combining deductive Automated Reasoning tools (no
 w 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 us
 e is in large theories\, i.e. on a large number of problems which in a con
 sistent fashion use many axioms\, lemmas\, theorems\, definitions and symb
 ols. The \nsystem works in cycles of theorem proving followed by machine l
 earning from successful proofs\, using the learned information to prune th
 e set of available axioms for the next theorem proving cycle. Although the
  metasystem is quite simple (ca. 1000 lines of Perl code)\, its design alr
 eady now poses quite interesting questions about the nature of thinking\, 
 in particular\, about how (and if and when) to combine learning from previ
 ous experience to attack difficult unsolved problems. The first version of
  MaLARea has been tested on the more difficult (chainy) division of the MP
 TP Challenge \n(http://www.cs.miami.edu/~tptp/MPTPChallenge/) solving 142 
 problems out of 252\, in comparison to E's 89 and SPASS 81 solved problems
 .\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR