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

• AI and big-data methods in theorem proving and mathematics
• Collaboration between automated and interactive theorem proving
• Common-sense reasoning and reasoning in science
• Alignment and joint processing of formal, semi-formal, and informal libraries
• Methods for large-scale computer understanding of mathematics and science
• Combinations of linguistic/learning-based and semantic/reasoning methods

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 Freer	Priors on propositions: towards probabilistic programming for theorem proving
Georges Gonthier	Formalising mathematical conventions
Thomas C. Hales	F-ABSTRACTS (formal abstracts) - project introduction and discussion
John Harrison	What has Artificial Intelligence Ever Done For Us (Formalizers)?
Andreas Holmstrom	Number-theoretic conjecturing via zeta types and Tannakian symbols
Michael Kohlhase	Tapping Sources of Mathematical (Big) Data
David McAllester	Models of Mentalese
Tim Rocktäschel	Deep Prolog: End-to-end Differentiable Proving in Knowledge Bases
Stephan Schulz	Deep Reasoning - A Vision for Automated Deduction
Luciano Serafini	Logic Tensor Networks
Martin Suda	Measuring progress to predict success: Can a good proof strategy be evolved?
Sarah Loos	Can 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

• Submission deadline: December 1, 2016
• Author notification: December 23, 2016
• Conference registration: January 20, 2017
• Camera-ready versions: February 1, 2017
• Conference: March 26-30, 2017

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 Arai	National Institute of Informatics
Jasmin Christian Blanchette	INRIA Nancy
Ulrich Furbach	University of Koblenz
Deyan Ginev	Jacobs University Bremen and Authorea
Thomas C. Hales (co-chair)	University of Pittsburgh
Sean Holden	University of Cambridge
Geoffrey Irving	Google
Cezary Kaliszyk (co-chair)	University of Innsbruck
Jens Otten	University of Oslo
Claudio Sacerdoti Coen	University of Bologna
Stephan Schulz (co-chair)	DHBW Stuttgart
Geoff Sutcliffe	University of Miami
Josef Urban (co-chair)	Czech Technical University in Prague

Arrival and departure

• A bus bringing the participants from Innsbruck to the conference center and back is provided.
• On Sunday the 26th the bus will depart from Innsbruck Central station at 10:45am, leave from the airport at 11:15 am and continue to Obergurgl.
• Please note the time change which happens in Europe on the night 25/26th March.
• If you want to join the bus at the train station look for the Info-Point. There, you will find the bus driver with the sign "University Center Obergurgl" as well as some of the University of Innsbruck organizers.
• If you want to join the bus at the airport, the bus will stop in front of the terminal, it will have the "Obergurgl" sign, and there will be organizers joining the bus as well.
• We expect to reach the conference center around 1pm, and after checking and lunch the first session will start at 3pm.
• On Thursday: check-out by 10am, bus leaves at 10:30, arrival in Innsbruck between 12:30 and 13:30 (depends on weather conditions and traffic). The bus will first stop at the airport and then in the city center (main railway station).

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

Pictures from the Conference

Acknowledgements and Sponsorship

We thank the University of Innsbruck for their support of the Obergurgl conference center.