The IJCAR 2004 Workshop on Empirically Successful First Order Reasoning (ESFOR (aka S4)) will be held at The 2nd International Joint Conference on Automated Reasoning Cork, Ireland, 4th July - 8th July, 2004

This workshop will bring together practioners and researchers who are concerned with the implementation and deployment of working automated reasoning systems for first order logic. The focus is on first order logic because it has adequate expressive power for many applications, has well understood and manageable computational properties. The automated reasoning community has much experience with the implementation and application of automated reasoning systems for the logic. As a result there exists, and is potential for further, empirically successful first order reasoning. The workshop will discuss "really running" systems, and not theoretical ideas that have not yet been translated into working systems. 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.

The workshop will be a 1.5 day workshop organized as follows:

• Afternoon day 1 - System papers
  • Invited speaker - Andrei Voronkov, The University of Manchester
  • Paper presentations
  • Panel discussion
  See the detailed schedule and abstracts.
• Morning day 2 - Application papers
  • Invited speaker - David Crocker, Escher Technologies
  • Paper presentations
  • Panel discussion
  See the detailed schedule and abstracts.
• Afternoon day 2 - System and application demonstrations
  See the detailed schedule and abstracts.

The workshop organizers are Geoff Sutcliffe, Stephan Schulz and Tanel Tammet. 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 refereed, 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 the following header:

\documentclass[a4paper,11pt]{article}
\textwidth  14.63cm
\textheight 22cm
\oddsidemargin  0.65cm
\evensidemargin 0.65cm
\topmargin  0.55cm
\headheight 0.0pt
\headsep    0.0pt

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 ESFOR workshop proceedings will be published in a volume of the ENTCS. Please prepare the camera ready version of your paper using the formatting instructions for ENTCS and the specially prepared entcsmacro.sty file, available from http://math.tulane.edu/~entcs/. Please take into account the input provided in your reviews. Your camera ready versions must be delivered as a .tar.gz file of the directory containing all the necessary files. Please email the .tar.gz to Geoff Sutcliffe - geoff@cs.miami.edu - by 30th May. This is a hard deadline.

Important dates

• Reviews due in from PC - 3rd May 2004
• Notification of acceptance - 10th May 2004
• Camera ready versions due - 30th May 2004
• Workshop - 4th and 5th July 2004

The International Journal of Artificial Intelligence Tools has agreed to a special issue based on extended versions of papers accepted to the workshop. The issue has been tentatively scheduled for June 2005. Authors of selected papers will be invited to submit extended versions, for reviewing according to IJAIT standards, before publication in the journal.

IJAIT Review Form