Browse our site
You are here:
Combining Machine Learning with Automated Rea...
Combining Machine Learning with Automated Reasoning in Large Formal Knowledge Bases
Josef Urban (Radboud University, Nijmegen, The Netherlands)
Wednesday, 6th of October 2010, 14h00
FCT/UNL, Seminar Room (Ed. II)
Induction (suggesting and learning conjectures, principles, and explanations from data) and deduction (drawing conclusions from principles) are two frequent reasoning methods used by humans. Recently, in the field of formal, computer-understandable mathematics, large formal knowledge bases have been created, allowing AI researchers to experiment with various novel combinations of inductive and deductive reasoning. At the same time, the search space of purely deductive general reasoning tools becomes very large when working over large mathematical theories, and needs to be complemented by various heuristics. A promising way how to automatically find and optimize such heuristics is again induction, and particularly machine learning from previous problems.
In this talk the field will be shortly introduced. The MaLARea system combining in a closed loop automated reasoning tools with machine learning from solved problems will be introduced, and evaluated on a large-theory benchmark. The various existing and possible ways of how to do machine learning over large bodies of computer-understandable mathematics will be discussed.
Josef Urban is a postdoc in the Foundations Group of ICIS at the Radboud University, Nijmegen. Before that he was an assistant professor at the Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague, and a Marie-Curie fellow at the Department of Computer Science at University of Miami.
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541