[DL] Artificial Intelligence and Theorem Proving
geoff at cs.miami.edu
Thu Nov 12 23:39:57 CET 2015
CALL FOR CONTRIBUTIONS
1st Conference on Artificial Intelligence and Theorem Proving,
April 3-6, 2016, Obergurgl, Austria
Deadline: December 12, 2015
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
- 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
- Methods for large-scale computer understanding of mathematics and
- Combinations of linguistic/learning-based and semantic/reasoning methods.
Sessions and Speakers
There will be three focused sessions on AI for ATP, ITP and mathematics, a
(tutorial) session on modern AI and big-data methods, and several sessions
with contributed talks. The focused sessions will be based on invited talks
and discussion oriented.
- AI and large-theory ATP/ITP.
Confirmed speakers: Thomas C. Hales
- AI and internal guidance of ATP.
Confirmed speakers: Robert Veroff, Stephan Schulz
- AI and automated understanding of informal and semi-formal mathematics.
Confirmed speakers: Noriko Arai, Deyan Ginev, Takuya Matsuzaki,
- Modern AI and big-data methods (tutorials/connections to ATP/ITP/math).
Confirmed speakers: Sean Holden, Christian Szegedy
We solicit 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=aitp2016)
by 12 December 2015. The authors will be notified of acceptance/rejection
by 23 December 2015.
Camera-ready versions of the accepted contributions, due by 1 February
2016, will be published in an informal book of abstracts for
distribution at the conference.
We will publish post-proceedings in an open-access series of
conference proceedings, such as LIPIcs, JMLR, or EPiC. Submission to
that volume will be open for everyone. Tentative submission deadline:
Marcos Cramer (Universiy of Luxembourg)
Thomas C. Hales (co-chair) (University of Pittsburgh)
Tom Heskes (Radboud University Nijmegen)
Sean Holden (University of Cambridge)
Cezary Kaliszyk (co-chair) (University of Innsbruck)
Ramana Kumar (University of Cambridge)
John Lafferty (University of Chicago)
Lawrence Paulson (University of Cambridge)
Stephan Schulz (co-chair) (DHBW Stuttgart)
Geoff Sutcliffe (University of Miami)
Josef Urban (co-chair) (Czech Technical University in Prague)
Location and Price
The conference will take place from April 3 to April 6 in the stunning
scenery of the Tyrolean Alps in the Obergurgl Conference Center
(http://www.uz-obergurgl.at/) of the University of Innsbruck. 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. The total price
for accommodation, food and registration for the four days will be around
Cezary Kaliszyk and Josef Urban
More information about the dl