Workshop on

Beyond SAT: What About First-Order Logic?

McGill University, Montreal, Canada, August 3, 2009

Call for Papers

The Workshop has been cancelled!
[ Background  |  Workshop Topic  |  Organizers  |  Invited Speakers  |  Program Committee  |  Submission  |  Publication  |  Important Dates ]


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.

Workshop Topic

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:

Invited Speakers

To be determined


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

Program Committee

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:

Submission is electronic only, through EasyChair. To submit, please go to 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.

Important Dates

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.