The Coq mailing list

[Josef Urban <josef.urban AT gmail.com>]

                     CALL FOR CONTRIBUTIONS

   1st Conference on Artificial Intelligence and Theorem Proving,
                            AITP 2016
                 April 3–6, 2016, Obergurgl, Austria

                     http://aitp-conference.org

       Deadline for extended abstracts: December 12, 2015
         https://easychair.org/conferences/?conf=aitp2016

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 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, Jiri Vyskocil
    - Modern AI and big-data methods (tutorials/connections to ATP/ITP/math).
      Confirmed speakers: Sean Holden, Christian Szegedy


Contributed talks

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.


Post-proceedings

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:
May 2016.


Programme committee

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 500 EUR.


Organizers

Cezary Kaliszyk and Josef Urban