The Coq mailing list

[geoff AT cs.miami.edu (Geoff Sutcliffe)]

                     CALL FOR CONTRIBUTIONS

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

                     http://aitp-conference.org

                    Deadline: 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