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).

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