AMI 2015

Automated Theorem Proving meets Interactive Theorem Proving

August 2, 2015, Berlin, Germany

A worskshop affiliated with CADE-25.

Aims and scope

The AMI workshop provides an informal platform for researchers interested in automated theorem proving (ATP) and interactive theorem proving (ITP), for instance, developers and users of ATP, SMT and similar systems, and developers and users of ITP systems such as Coq, HOL, Isabelle or Mizar. Its aim is the exchange of experiences and ideas for pushing these technologies further into the mainstream: to explore methods or tools from ATP that could be benefit ITP and vice versa; to advance the integration and convergence of these technologies, e.g. by considering tools and techniques from mathematics, programming languages or AI; to bring ATP and ITP work flows closer to mathematical and engineering practice.

Workshop topics include:


To foster discussions, we ask for submissions of extended abstracts of 2 to 4 pages as well as for full papers of at most 15 pages. If submissons are based on previously published material that should be stated clearly. Presentations will be selected based on the quality of their contribution and their relevance to the workshop. All accepted submissions will be published online at the workshop web site. Quality of submissions permitting, we are planning their consideration for a journal special issue after the workshop. Papers must be submitted via EasyChair.

Important dates

We regret to inform that due to a low number of submissions, we have decided to cancel the workshop.

Program committee

Invited speakers (joint with the PxTP workshop)