The CADE-20 Workshop on

Empirically Successful
Classical Automated Reasoning

will be held 22nd-23rd July, at

The 20th International Conference on Automated Deduction
Tallinn, Estonia, 22nd July - 26th July, 2005

This workshop will bring together practioners and researchers who are concerned with the implementation and deployment of working automated reasoning systems for classical logic (propositional, first order, and higher order). The focus is on classical logic because it has adequate expressive power for many applications, has well understood and manageable computational properties, and the automated reasoning community has much experience and success with the implementation and application of automated reasoning systems for classical logics. Consequently, there exist empirically successful classical automated reasoning systems and applications. The workshop will discuss "really running" systems and applications, and not theoretical ideas that have not yet been translated into working software. The workshop will have two main topic areas:



Additionally, the workshop will include system and application demonstrations. Demonstrations of systems and applications described in paper presentations, and demonstrations of systems and applications without an accompanying paper, are both encouraged.

Participants are expected from several sources:

Among the concrete application areas we envision users active in the fields of verification, deductive databases, mathematics, knowledge representation, semantic web, etc. The workshop will provide a forum for discussion of the techniques necessary to take automated reasoning from the lab and into the "real world". The workshop will enable the attendees to learn from each others' practical experiences, and will document their state-of-the-art techniques.

ESCAR is the successor to the successful ESFOR workshop held at IJCAR 2004 - see the abstracts of the papers accepted into ESFOR.


The workshop will be a 1 day workshop (spread over 2 days), organized as follows:

See the schedule of presentation for the accepted papers, and the abstracts of the accepted papers.

Program Committee
System papers Application papers
Matt Kaufmann
Bernd Löchner
Bill McCune
Monty Newborn
Larry Paulson
Silvio Ranise
Alexandre Riazanov
Stephan Schulz
Carsten Schürmann
Laurent Simon
Bernhard Beckert
Nikolaj Bjørner
Koen Claessen
Bernd Fischer
Ulrich Furbach
Greg Nelson
Geoff Sutcliffe

The workshop organizers are Geoff Sutcliffe, Stephan Schulz and Bernd Fischer. If you have any questions about the workshop, please email the organizers.


Submission of papers for presentation at the workshop, and proposals for system and application demonstrations at the workshop, are now invited. Submissions will be reviewed (using this review form), and a balanced program of high-quality contributions will be selected. Submissions can be in PDF or Postscript, and must conform to the format produced by LaTeX with this template. There is a 20 page limit. Long listings of problems or computer output should be relegated to a referenced WWW site.

Proposals for system and application demonstrations must include:

Submission is via EasyChair (thanks to Andrei Voronkov).

Final Version Instructions

The ESCAR workshop proceedings will be published by CADE-20. Please prepare the final version of your paper using the formatting instructions above, taking into account the input provided in your reviews. Your final versions must be delivered as a .tar.gz file of the directory containing all the necessary files, including a .pdf version. Please email the .tar.gz to Geoff Sutcliffe - by 20th June. This is a hard deadline.

Important dates

Journal Publication

The Journal of Automated Reasoning has agreed to a special issue on emperically successful automated reasoning. Authors of ESCAR papers will be able to submit extended versions of their workshop papers for this special issue. All papers submitted for the special issue will be reviewed according to the journal's standards. See the Call for Papers for more details.