## CADE-22## Workshop on## Beyond SAT: What About First-Order Logic? McGill University, Montreal, Canada, August 3, 2009 ## Call for Papers |

The arguably most successful branch of automated reasoning today is
(propositional) SAT solving. Propositional encodings and SAT solvers
are widely used in AI and formal methods to solve problems from
planning, diagnosis, knowledge compilation, constraint satisfaction,
just to name a few, and they dominate the whole area of software and
hardware verification for embedded reasoning services. However, while
the success of *reducing* problems to propositional logic is
undeniable, many problems are more naturally formulated in a more
expressive logic. For instance, constraint satisfaction problems,
bounded model checking and bit-vector arithmetic problems can often be
encoded more succinctly in a restricted fragment of first-order, EPR
(Essentially Propositional Reasoning, equivalent to the
Bernays-Schönfinkel class). Instance-based methods for first-order
logic, which natively
decide EPR in a non-trivial way, can then be
considered for beneficial use in problem formulation and reasoning.
Similarly, Description Logics are widely used as logical underpinning
of ontology languages such as OWL, which has led to the design and
investigations of a number of interesting reasoning approaches and
novel reasoning problems.

This workshop is centered around the question whether (fragments of)
logics more expressive than propositional logic, in particular
first-order logic, can *directly* be
used for problem formulation and
reasoning in the areas that are dominated by propositional methods
today. This question becomes non-trivial under the conditions that the
use of these logics shall address shortcomings of the
propositional approach, such as lack of expressivity and scalability,
while not compromising efficiency. We perceive this as a long-term
research challenge.

The workshop solicits contributions towards this challenge. The topic list includes (but is not limited to) the following:

- Innovative encodings of application problems in AI and formal methods into logics more expressive than propositional logic
- Problem solving with EPR: reductions from e.g. planning, bounded model checking, QBF, description and modal logics into EPR; calculi and systems for EPR and extensions like theory reasoning, equality
- Finite model finders, in particular based on encodings into tractable fragments of first-order logic
- Transfer of techniques developed for propositional SAT or for constraint satisfaction to theorem provers for more expressive logics
- Implementation techniques and implementations
- Practical applications and reports on success/failure of first-order methods
- EPR Benchmark problems (the TPTP doesn't have enough)

Peter Baumgartner, NICTA Canberra, Australia (main contact)

Nikolaj Bjorner, Microsoft Research, USA

Koen Claessen, Chalmers University, Sweden

Konstantin Korovin, The University of Manchester, UK

Juan Antonio Navarro Pérez, MPI-SWS, Germany

Cesare Tinelli, The University of Iowa, USA

Peter Baumgartner, NICTA

Nikolaj Bjorner, Microsoft Research

Alessandro Cimatti, IRST - Istituto per la Ricerca Scientifica e Tecnologica

Koen Claessen, Chalmers University

Enrico Giunchiglia, Dipartimento di Informatica, Sistemistica e Telematica

Konstantin Korovin, The University of Manchester

Joao P. Marques Silva, University College Dublin

Leonardo de Moura, Microsoft Research

Juan Antonio Navarro Pérez, MPI-SWS

Ilkka Niemelae, Helsinki University of Technology

Robert Nieuwenhuis, Technical University of Catalonia

Hans de Nivelle, University of Wroclaw

David Plaisted, University of North Carolina at Chapel Hill

Andrey Rybalchenko, MPI Softwaresystems

Ulrike Sattler, The University of Manchester

Cesare Tinelli, The University of Iowa

Andrei Voronkov, The University of Manchester

There are two submission categories:

**Previously unpublished work.**

Beside mature work, we also solicit preliminary work or work in progress. Submissions should not exceed 15 printed pages. The final versions of the selected contributions will be collected in the workshop proceedings.**Presentation-only papers of previously published work.**

The intent of presentation-only papers is to allow authors to make their recently published work known to a wider audience. Participants who wish to submit in this category should provide a summary of up to 3 pages and an indication where the paper has appeared, or is expected to appear. The abstracts of the presentation-only papers will be included in the workshop proceedings, but the papers themselves will not be included.

*Submission is electronic only*,
through EasyChair.
To submit, please go to http://www.easychair.org/conferences/?conf=beyondsat09.
Please use the EasyChair LaTeX class file, avalable
here.

The (informal) workshop proceedings will be distributed at the workshop and made available on the internet.

May 17: paper submissions deadline

June 12: notification of acceptance

July 5: final versions due

August 3: workshop date

For further information on the workshop, please contact any of the organisers.