Day-1, 11 April 2013

Machine Learning in Automated Reasoning

10:30-11:00 Registration, Queen Mother Building.
11:00-11:30 Welcoming Coffee Session
(Time for participants to place their Research Posters on stands)
11.30-12.30 Invited Speaker 1. Chair: Katya Komendantskaya. Video of the session. 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 .
12:30-13:30 Lunch, School of Computing, Queen Mother Building.
Poster Discussion
13:30-15:30 Regular Talks, 15 min each + 5 min questions.
Session 1: Machine Learning in Automated Reasoning.
Chair: Josef Urban. Video of the session.
15:30-16.00 Coffee Break.
Poster Discussion
16.00-16.30 Discussion Panel 1. Chair: Ursula Martin. Video of the session.
  • Machine Learning in Automated Reasoning.
Free Format.
16.30-17.30 Poster Session.
19.00 - Dinner, in Apex Hotel.


Day-2, 12 April 2013

09.30-10.30 Invited Speaker 2. Chair: Alexander Bolotov. Video of the session. Slides. 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.
10.30-11.00 Discussion Panel 2. Chair: Manfred Kerber. Free Format.
11:00-11:30 Coffee Break
Poster Discussion
11:30-12:30 Regular Talks, 15 min each + 5 min questions.
Session 2: Temporal and Modal Logics.
Chair: Lilia Georgieva. Video of the session.
12:30-13:30 Lunch, School of Computing, Queen Mother Building.
Poster Discussion
13:30-15:30 Regular Talks, 15 min each + 5 min questions. Video of the sessions.
Session 3: Non-monotonic and Paraconsistent Logics for Automated Reasoning. Chair: Renate Schmidt. Session 4: Model Checking in Automated Reasoning. Chair: Anthony Lin. Session 5: TABLEAUX and Calculi in Automated Reasoning. Chair: Roy Dyckhoff.
15:30-16.00 Coffee Break.
Poster Discussion
16:00-17:00 Regular Talks, 15 min each + 5 min questions.
Session 6: Constraint Solving in Automated Reasoning.
Chair: Peter Nightinghale. Video of the session.