CADE-22Workshop onBeyond SAT: What About First-Order Logic?McGill University, Montreal, Canada, August 3, 2009Call 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.
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:
To be determined
Organizers
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:
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.
Publication
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.