CALL FOR WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS, AND PAPERS

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

http://www.cade-25.info

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


CALL FOR WORKSHOPS

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?


CALL FOR TUTORIALS

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.


CALL FOR SYSTEM COMPETITIONS

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?


CALL FOR PAPERS

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

http://www.springer.de/comp/lncs/authors.html

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).


IMPORTANT DATES

Workshop/Tutorials/System Competitions:

Submission deadline: 14 November 2014
Notification: 28 November 2014

Papers:

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
Competitions: 1 to 7 August 2015
Conference: 3 August (afternoon) to 7 August 2015


SUBMISSION INSTRUCTIONS

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

https://easychair.org/conferences/?conf=cade25workshopstutor

Papers should be submitted via

https://easychair.org/conferences/?conf=cade25


CADE-25 ORGANIZERS

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