A more detailed schedule is now available here.


Thursday 11th April 2013

11:00-11:30: Coffee.
11:30-12:30: Invited lecture: Josef Urban. AI over Large Formal Knowledge Bases: The First Decade

Abstract: March 2003, the first version of the Mizar Problems for Theorem Proving (MPTP) was released. In the past ten years, such large formal knowledge bases have started to provide an interesting playground for combining deductive and inductive AI methods. The talk will discuss three related areas of application in which machine learning and general AI have been recently experimented with: (i) premise selection for theorem proving over large formal libraries built with systems like Mizar, HOL Light, and Isabelle (ii) advising and tuning first-order automated theorem provers such as E and leanCoP, and (iii) building larger inductive/deductive AI systems such as MaLARea .

Bio: Josef Urban (Radboud University Nijmegen) is a Czech computer scientist and mathematician working mainly on automated reasoning and AI methods for large formal (computer-understandable) knowledge bases. His work includes export of the formal Mizar Mathematical Library (MML) to formats suitable for first-order automated theorem provers (ATPs), development of automated methods and systems for AI/ATP-based advising over MML and Flyspeck (MoMM, Mizar Proof Advisor, MizAR, HOL(y)Hammer), creation of AI/ATP benchmarks and competition designs such as MPTP Challenge, CASC LTB, MPTP2078, and Mizar@Turing, and development of general AI/ATP methods and systems for reasoning in large theories (MaLARea, MaLeCoP, BliStr).

12:30-13:30: Lunch.
13:30-15:30: Session 1. Machine Learning in Automated Reasoning.
15:30-16:00: Coffee.
16:00-16:30: Discussion Panel 1. Machine Learning in Automated Reasoning.
16:30-17:30: Poster session.
19:00- : Dinner at the Apex City Quay Hotel.

Friday 12th April 2013


09:30-10:30: Invited lecture: Manfred Kerber. ForMaRE –- Formal Mathematical Reasoning in Economics.

Abstract: We present the ForMaRE project which applies FORmal MAthematical Reasoning to Economics. Theoretical economics makes use of mathematical proof and we seek to increase confidence in these theoretical results by applying formal mathematical reasoning. This will lead on the one hand to new challenge problems in formal reasoning. On the other hand we are conducting research that connects economics and formal methods. We will discuss some areas of interest such as game theory and auctions, where we are currently building a toolbox of formalizations.

Bio: Manfred Kerber did his PhD at the University of Kaiserlautern, Germany, on the Representation of Mathematical Concepts and their Translation into First Order Logic. He was for a few years Senior Research Fellow at the University of Saarbruecken working on the Omega project. Since 1996 he has been a university lecturer at the University of Birmingham. He has interests in aspects of representation, reasoning, heuristics, machine learning and since a few years he has been involved in interdisciplinary work in theoretical economics. Since May 2012 he has been working in the ForMaRE project on Formal Mathematical Reasoning in Economics.

10:30 - 11:00. Discussion Panel 2. Automated Reasoning in Economics.
11:00 - 11:30. Coffee Break.
11:30 - 12:30. Session 2: Temporal and Modal Logics.
12:30 - 13:30. Lunch.
13:30-15:30. Session 3: Non-monotonic and Paraconsistent Logics for Automated Reasoning.
Session 4: Model Checking in Automated Reasoning.
Session 5: TABLEAUX and Calculi in Automated Reasoning.
15:30-16:00. Coffee.
16:00-17:00. Session 6: Constraint Solving in Automated Reasoning