[DL] CFP: CADE-22 Workshop 'Beyond SAT: What About First-Order Logic?'

[Peter Baumgartner]

=================================================================

                          CADE-22 Workshop on

                Beyond SAT: What About First-Order Logic?

          McGill University, Montreal, Canada, August 3, 2009 

                            CALL FOR PAPERS

=================================================================


Background
----------
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:

- 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)

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

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 deNivelle,                 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

Submission
----------
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.

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

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

Workshop home page: http://users.rsise.anu.edu.au/~baumgart/beyond-SAT/

-- 
Peter Baumgartner                   Ph: +61 2 6267 6217
NICTA, Canberra Research Lab, and   http://nicta.com.au/
The Australian National University  http://rsise.anu.edu.au/~baumgart/