CFP: CADE Workshops, Tutorials, System Competitions, Papers


25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015

Submission deadlines:

  • 14 November 2014 (workshops/tutorials/competitions)
  • 16/23 February 2015 (papers)

CADE is the major international forum at which research on all aspects of automated deduction is presented. The 25th jubilee edition will feature a special session on the past, present, and future of automated deduction with

  •   Ursula Martin      University of Oxford
  •   Frank Pfenning     Carnegie Mellon University
  •   David Plaisted     University of North Carolina at Chapel Hill
  •   Andrei Voronkov    University of Manchester

as invited speakers. In addition, there will be invited presentations by

  •   Ulrich Furbach     University of Koblenz
  •   Edward Zalta       Stanford University

Workshop proposals for CADE-25 are solicited. Both well-established workshops and newer ones are encouraged. Similarly, proposals for workshops with a tight focus on a core automated reasoning specialization, as well as those with a broader, more applied focus, are very welcome.
Please provide the following information in your application document:

  • Workshop title.
  • Names and affiliations of organizers.
  • Proposed workshop duration (from half a day to two days) and preferred day(s).
  • Brief description of the goals and the scope of the workshop. Why is the workshop relevant for CADE?
  • Is the workshop new or has it met previously? In the latter case information on previous meetings should be given (e.g., links to the program, number of submissions, number of participants).
  • What are the plans for publication?

Tutorial proposals for CADE-25 are solicited. Tutorials are expected to be half-day events, with a theoretical or applied focus, on a topic of interest for CADE-25. Proposals should provide the following information:

  • Tutorial title.
  • Names and affiliations of organizers.
  • Brief description of the tutorial’s goals and topics to be covered.
  • Whether or not a version of the tutorial has been given previously.

CADE will take care of printing and distributing notes for tutorials that would like this service.

The CADE ATP System Competition (CASC), which evaluates automated theorem proving systems for classical logics, has become an integral part of the CADE conferences.

Further system competition proposals are solicited. The goal is to foster the development of automated reasoning systems in all areas relevant for automated deduction in a broader sense. Proposals should include the following information:

  • Competition title.
  • Names and affiliations of organizers.
  • Duration and schedule of the competition.
  • Room/space requirements.
  • Description of the competition task and the evaluation procedure.
  • Is the competition new or has it been organized before? In the latter case information on previous competitions should be given.
  • What computing resources are required and how will they be provided?

High-quality submissions on the general topic of automated deduction, including foundations, applications, implementations, and practical experiences are solicited.

  • Logics of interest include propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, constructive, other non-classical, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof.
  • Paradigms of interest include theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their  integration.
  • Methods of interest include resolution, superposition, completion, saturation, term rewriting, decision procedures, model elimination, connection methods, tableaux, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including matching, unification, orderings, induction, indexing techniques, proof presentation and explanation, proof planning.
  • Applications of interest include program analysis, verification and synthesis of software and hardware, formal methods, computational logic, computer mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, declarative programming, robotics, planning, and other areas of AI.

Submissions can be made in the categories regular papers and system descriptions. The page limit in Springer LNCS style is 15 pages for regular papers and 10 pages for system descriptions. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on
relevance, originality, significance, correctness, and readability. System descriptions should contain a link to a working system and will also be judged on usefulness and design. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. Reviewers will be encouraged to consider this additional material, but submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at

At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award.

At CADE-25 we also intend to award the best student paper (details will follow).


Workshop/Tutorials/System Competitions:

  • Submission deadline:      14 November 2014
  • Notification:             28 November 2014


  • Abstract deadline:        16 February 2015
  • Submission deadline:      23 February 2015
  • Rebuttal phase:           15-18 April 2015
  • Notification:             26 April 2015
  • Final version:            17 May 2015

Workshops and Tutorials:

  • 1 August to 3 August (morning) 2015


  • 1 to 7 August 2015


  • 3 August (afternoon) to 7 August 2015

Proposals for workshops, tutorials, and system competitions should be uploaded via

Papers should be submitted via


Conference Chair:
Christoph Benzmüller   Freie Universität Berlin

Program Committee Co-Chairs:
Amy Felty              University of Ottawa
Aart Middeldorp        University of Innsbruck

Workshop, Tutorial, and Competition Co-Chairs:
Jasmin Blanchette      Technische Universität München
Andrew Reynolds        EPFL Lausanne

Publicity and Web Chair:
Julian Röder           Freie Universität Berlin

Program Committee
Carlos Areces          Universidad Nacional de Córdoba
Alessandro Armando     University of Genova
Christoph Benzmüller   Freie Universität Berlin
Josh Berdine           Microsoft Research
Jasmin Blanchette      Technische Universität München
Marta Cialdea Mayer    Universita di Roma Tre
Stephanie Delaune      CNRS
Gilles Dowek           Inria
Amy Felty              University of Ottawa
Reiner Hähnle          Technical University of Darmstadt
Stefan Hetzl           Vienna University of Technology
Marijn Heule           The University of Texas at Austin
Nao Hirokawa           JAIST
Ullrich Hustadt        University of Liverpool
Deepak Kapur           University of New Mexico
Gerwin Klein           NICTA and UNSW
Laura Kovács           Chalmers University of Technology
Carsten Lutz           Universität Bremen
Assia Mahboubi         Inria
Aart Middeldorp        University of Innsbruck
Albert Oliveras        Technical University of Catalonia
Nicolas Peltier        CNRS
Brigitte Pientka       McGill University
Ruzica Piskac          Yale University
André Platzer          Carnegie Mellon University
Andrew Reynolds        EPFL Lausanne
Christophe Ringeissen  LORIA-INRIA
Renate Schmidt         University of Manchester
Stephan Schulz         DHBW Stuttgart
Georg Struth           University of Sheffield
Geoff Sutcliffe        University of Miami
Alwen Tiu              Nanyang Technological University
Freek Wiedijk          Radboud University Nijmegen