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.
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.
|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?|
|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|
The (extended) abstracts of all the invited and contributed talks are now available online.
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).
|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|
|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|
|13:00-15:00||lunch and check-in|
What has Artificial Intelligence Ever Done For Us (Formalizers)?
Deep Reasoning - A Vision for Automated Deduction
Can Deep Learning Help Formal Reasoning?
Deep Prolog: End-to-end Differentiable Proving in Knowledge Bases
Formalising mathematical conventions
Thomas C. Hales
F-ABSTRACTS (formal abstracts) - project introduction and discussion
Tapping Sources of Mathematical (Big) Data
Josef Urban and Jiri Vyskocil
Progress in Automating Formalization
Number-theoretic conjecturing via zeta types and Tannakian symbols
DeepAlgebra - an outline of a program
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
Logic Tensor Networks
Mathematics, Ontology and Reference
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
Towards Smart Proof Search for Isabelle
AITP Discussion or free time
Priors on propositions: towards probabilistic programming for theorem proving
Measuring progress to predict success: Can a good proof strategy be evolved?
Jan Jakubuv and Robert Veroff
Towards AI Methods for Prover9
Monte Carlo Connection Prover
Problems from the Grundlagen
Logic-Independent Premise Selection for Autormated Theorem Proving
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
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.
If you stay in Innsbruck before/after the conference, we recommend the following hotels, we have good experience with
You can rent skis/snowboards/boots/helmets in Obergurgl or already in
Innsbruck. It might be hard to rent clothing in Obergurgl, but it is
possible in Innsbruck (e.g., here).
Ski+Boots rental per day: 30-50Euros per day (depending on the quality).
Obergurgl daily ski passes: From noon: 40Euros. From 11am: 45Euros. 3 days: 143Euros
Here are two photos from the previous year showing the skiing conditions and the village (with the conference center hidden on the right side of the photo) taken in April.
|We thank the University of Innsbruck for their support of the Obergurgl conference center.|