2nd Conference on Artificial Intelligence and Theorem Proving

AITP 2017

March 26–30, 2017, Obergurgl, Austria

Registration is already closed. See below for the list of talks, schedule and local information

Background

Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.

Topics

Sessions

There will be several focused sessions on AI for ATP, ITP and mathematics, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented.

Invited talks

Cameron FreerPriors on propositions: towards probabilistic programming for theorem proving
Georges GonthierFormalising mathematical conventions
Thomas C. HalesF-ABSTRACTS (formal abstracts) - project introduction and discussion
John HarrisonWhat has Artificial Intelligence Ever Done For Us (Formalizers)?
Andreas HolmstromNumber-theoretic conjecturing via zeta types and Tannakian symbols
Michael Kohlhase Tapping Sources of Mathematical (Big) Data
David McAllesterModels of Mentalese
Tim RocktäschelDeep Prolog: End-to-end Differentiable Proving in Knowledge Bases
Stephan SchulzDeep Reasoning - A Vision for Automated Deduction
Luciano SerafiniLogic Tensor Networks
Martin SudaMeasuring progress to predict success: Can a good proof strategy be evolved?
Sarah LoosCan Deep Learning Help Formal Reasoning?

Contributed talks

Alexander Bentkamp, Jasmin Christian Blanchette and Dietrich Klakow: An Isabelle Formalization of the Expressiveness of Deep Learning
Chad Brown: Problems from the Grundlagen
Przemyslaw Chojecki: DeepAlgebra - an outline of a program
Joe Corneli and Moritz Schubotz: math.wikipedia.org: A vision on a collaborative semi-formal, language independent math(s) encyclopedia
Michael Färber, Cezary Kaliszyk and Josef Urban: Monte Carlo Connection Prover
Jan Jakubuv, Josef Urban and Robert Veroff: Towards AI Methods for Prover9
Eugen Kuksa: Logic-Independent Premise Selection for Autormated Theorem Proving
Ramana Kumar and Benya Fallenstein: Applying Formal Verification to Reflective Reasoning
Yutaka Nagashima Towards Smart Proof Search for Isabelle
Karol Pąk and Aleksy Schubert: Greedy Algorithms for Finding Maximum Number of Then Step in Reasoning
Bruno Woltzenlogel Paleo and John Slaney: Proof Search in Conflict Resolution
Marwin Segler and Mark Waller: Chemical Discovery as a Knowledge Graph Completion Problem
Josef Urban and Jiri Vyskocil: Progress in Automating Formalization

Dates

AITP solicits contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2017). Accepted contributions will be published in an informal book of abstracts for distribution at the conference.

Informal proceedings

The (extended) abstracts of all the invited and contributed talks are now available online.

Post-proceedings

We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR).

Program Committee

Noriko AraiNational Institute of Informatics
Jasmin Christian BlanchetteINRIA Nancy
Ulrich FurbachUniversity of Koblenz
Deyan GinevJacobs University Bremen and Authorea
Thomas C. Hales (co-chair)University of Pittsburgh
Sean HoldenUniversity of Cambridge
Geoffrey IrvingGoogle
Cezary Kaliszyk (co-chair)University of Innsbruck
Jens OttenUniversity of Oslo
Claudio Sacerdoti CoenUniversity of Bologna
Stephan Schulz (co-chair)DHBW Stuttgart
Geoff SutcliffeUniversity of Miami
Josef Urban (co-chair)Czech Technical University in Prague

Arrival and departure

Program (preliminary)



March 26
13:00-15:00 lunch and check-in
15:00-16:30 Welcome

John Harrison
What has Artificial Intelligence Ever Done For Us (Formalizers)?

Stephan Schulz
Deep Reasoning - A Vision for Automated Deduction

16:30-17:00 coffee break
17:00-18:30 Sarah Loos
Can Deep Learning Help Formal Reasoning?

Tim Rocktäschel
Deep Prolog: End-to-end Differentiable Proving in Knowledge Bases

19:00 dinner


March 27
8:30-10:00 Georges Gonthier
Formalising mathematical conventions

Thomas C. Hales
F-ABSTRACTS (formal abstracts) - project introduction and discussion

10:00-10:30 coffee break
10:30-11:45 Michael Kohlhase
Tapping Sources of Mathematical (Big) Data

Josef Urban and Jiri Vyskocil
Progress in Automating Formalization

11:45-16:00 free time
16:00-16:30 coffee break
16:30-18:45 Andreas Holmstrom
Number-theoretic conjecturing via zeta types and Tannakian symbols

Przemyslaw Chojecki
DeepAlgebra - an outline of a program

short break


Marwin Segler and Mark Waller
Chemical Discovery as a Knowledge Graph Completion Problem

Joe Corneli and Moritz Schubotz
math.wikipedia.org: A vision on a collaborative semi-formal, language independent math(s) encyclopedia

19:00 dinner


March 28
8:30-10:00 Luciano Serafini
Logic Tensor Networks

David McAllester
Mathematics, Ontology and Reference

10:00-10:30 coffee break
10:30-12:00 Ramana Kumar and Benya Fallenstein
Applying Formal Verification to Reflective Reasoning

Alexander Bentkamp, Jasmin Christian Blanchette and Dietrich Klakow
An Isabelle Formalization of the Expressiveness of Deep Learning

Yutaka Nagashima
Towards Smart Proof Search for Isabelle

12:00-17:20 free time
17:20-18:30
AITP Discussion or free time

19:00 dinner


March 29
8:30-10:00 Cameron Freer
Priors on propositions: towards probabilistic programming for theorem proving

Martin Suda
Measuring progress to predict success: Can a good proof strategy be evolved?

10:00-10:30 coffee break
10:30-11:30 Jan Jakubuv and Robert Veroff
Towards AI Methods for Prover9

Michael Färber
Monte Carlo Connection Prover

11:30-16:00 free time
16:00-16:30 coffee break
16:30-18:40 Chad Brown
Problems from the Grundlagen

Eugen Kuksa
Logic-Independent Premise Selection for Autormated Theorem Proving

short break


Karol Pąk and Aleksy Schubert
Greedy Algorithms for Finding Maximum Number of Then Step in Reasoning

Bruno Woltzenlogel Paleo and John Slaney
Proof Search in Conflict Resolution

19:00 dinner


Location, Prices and Further Local Information

The conference will take place from March 26 to March 30 in the stunning scenery of the Tyrolean Alps in the Obergurgl Conference Center of the University of Innsbruck. The pictures of the rooms are here. Obergurgl is a picturesque village located at an altitude of 2000m, a 1-hour drive from Innsbruck. It offers a variety of winter-sport activities such as skiing, snowshoeing and hiking at this time of the year.

Hotels in Innsbruck

If you stay in Innsbruck before/after the conference, we recommend the following hotels, we have good experience with