The CADE-21 Workshop on

Empirically Successful
Automated Reasoning in Large Theories
(ESARLT)

will be held on 15th July 2007, as part of

The 21st International Conference on Automated Deduction
Bremen, Germany, 15th - 20th July, 2007

This workshop brings together practioners and researchers who are concerned with the development and application of automated reasoning in large theories - theories in which ...

In large theories it is useful to develop and apply intelligent reasoning techniques that go beyond "black box" reasoning, to include techniques for selecting axioms, using proved theorems as lemmas, etc. Reasoning in all forms (automated, interactive, etc) and all logics (classical, non-classical, all orders, etc) is of interest to the workshop. The workshop will discuss only "really running" systems and applications, and not theoretical ideas that have not yet been translated into working software. The workshop has two main topic areas:

Systems

Applications

Additionally, the workshop includes 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 provides a forum for discussion of the techniques necessary to take automated reasoning from the lab and into the "real world" of large theories. The workshop will enable the attendees to learn from each others' practical experiences, and will document their state-of-the-art techniques.

ESARLT is the successor to the successful ESFOR, ESCAR, ESHOL, and ESCoR workshops. Financial support for the invited speakers has been provided by Microsoft Research.

Organization

The workshop will be a one day workshop, organized as follows:

The proceedings are now available here, and as CEUR Workshop Proceedings 257. The proceedings may be cited as:
@Proceedings{SUS07,
    Author       = "Sutcliffe, G. and Urban, J. and Schulz, S.",
    Year         = "2007",
    Title        = "{Proceedings of the CADE-21 Workshop on Empirically
                    Successful Automated Reasoning in Large Theories}",
    Place        = "Bremen, Germany",
    Series       = "CEUR Workshop Proceedings",
    Volume       = "257",
    ISSN         = "ISSN 1613-0073"
}

Program Committee
Serge Autexier
Bernhard Beckert
Johann Belinfante
Nikolaj Bjørner
Simon Colton
 Jon Curtis
Ingo Dahn
Stefan Decker
Hans de Nivelle
Bernd Fischer
 Jia Meng
Erik Mueller
Michael Norrish
Larry Paulson
Adam Pease
 Petr Pudlak
Wolfgang Reif
Alexandre Riazanov
Stephan Schulz
Geoff Sutcliffe
 Dmitry Tsarkov
Josef Urban
Uwe Waldmann
Freek Wiedijk

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

Journal Publication

The Journal of Symbolic Computation has agreed to a special issue based around around the topic of the ESARLT workshop. The special issue will target ESARLT participants, but will also also accept submissions from the broader community. A call for papers will be made after the workshop papers have been selected.

$100 Challenges

The MPTP $100 Challenges are examples of automated reasoning problems in large theories. The winners of the challenges will be announced at the ESARLT workshop.

The Modal Logic $100 Challenge can be an example of automated reasoning in a large theory. The winner of the challenge will be announced at the ESARLT workshop.

Submission

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, and a balanced program of high-quality contributions will be selected. Submissions must be in PDF, and must conform to the format produced by LaTeX with this template (this is what the PDF should look like). 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). The selected contributions will be printed as workshop proceedings, and will also be published as CEUR Workshop Proceedings.

 The (new, extended) submission deadline is 18th May 2007

Important dates