The CADE-20 Workshop on Empirically Successful Classical Automated Reasoning (ESCAR) 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:

Systems

• Implementation techniques and comparisons
• Data structures and algorithms for the efficient representation of terms, formulae, search states, etc., e.g. new indexing techniques, efficient implemetation of simplification orderings, etc.
• Higher level data structures and formats for the representation of proof tasks and derivations, proof and lemma storage, etc.
• Implemented and evaluated heuristics

• Descriptions of automated reasoning solutions in application domains
• Experiences with practical applications
• Encoding of domain problems into logic, and decoding of logic solutions into the domain
• Special automated reasoning techniques for applications
• User interfaces (to whole systems, not just the automated reasoning component)
• System integration

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:

• Researchers who have developed and implemented successful automated reasoning techniques and systems.
• Practioners who have deployed automated reasoning systems in working applications.
• Users who have already attempted to apply automated reasoning in their domains, and now wish to learn more.
• Potential users who are interested in learning how automated reasoning may be used in their domains.

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:

• Afternoon day 1 - Application papers
  • Invited speaker - Byron Cook, Microsoft Research
  • Paper presentations
• Morning day 2 - System papers
  • Invited speaker - Niklas Sörensson, Chalmers University of Technology
  • Paper presentations
  • Panel discussion: What Tools and Structures are Needed for more Empirically Successful Classical Automated Reasoning?
    Panelists: Byron Cook, John Slaney, Andrei Voronkov

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:

• System name, developers names and contact details
• A system description, or associated paper submission
• Evidence that the system or application is empirically successful
• Screen shots or information for online access
• Details of hardware and software that will have to be provided by the organizers if the demonstration is approved

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

• Submission deadline - 9th May 2005
• Papers distributed to PC - 10th May 2005
• Reviews due in from PC - 25th May 2005
• Notification of acceptance - 30th May 2005
• Camera ready versions due - 20th June 2005
• Workshop - 22nd and 23rd July 2005

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.