Methods for deciding satisfiability or satisfaction are of utter importance for both the theoretical relevance and practical impact of a logic. Description logics in knowledge representation and temporal logics in program verification for example have only gained popularity because of efficient decision procedures for them. Different logics require different decision procedures. Nevertheless, certain methodologies have proved to be successful in providing decidability results for several, even quite different logics. Terminating semantic tableaux have served for a long time as one of the practically most useful and efficient types of decision procedures for a wide range of logical systems. Over the past two decades automata-based methods for testing satisfiability and model checking for various modal and temporal logics have gained very wide recognition and popularity. They provide uniform, elegant, and often optimal decision procedures. Games provide a very intuitive access to understanding and possibly also circumventing the technical difficulties posed by the decision problem for a certain logic. Reductions to SAT/SMT problems can yield very efficient procedures in practice. Furthermore, there are other methodologies like resolution, reductions, etc. Perception of some methodology being better than others has grown within certain communities, for example regarding automata-based techniques in automatic verification or tableau-based techniques in knowledge representation. Such perception, however, is not based on systematic comparative analysis, and sometimes practical experience with well-designed tools suggests that such perception can also be misleading. Moreover, various optimization techniques, such as on-the-fly methods for example draw automata-based algorithms very close to tableau-like procedures, thus strongly suggesting that tableaux and automata for instance are closely related. Yet, few formal technical results to that effect are known, and the scientific discussions on the pros and cons, and similarities and differences between different methodologies have been rather sporadic so far. The purpose of this workshop is to provide an expert forum for such discussion, to provoke and foster discussion between communities, and to stimulate further research on the topic. The workshop welcomes contributions on comparisons between different methods, exhibiting differences or similarities, in theory or in practice, in general or with respect to a certain logic.
More information can be found here.
- Moshe Vardi, Rice University, TX, US: Symbolic Techniques in Propositional Satisfiability Solving
- Jerome Leroux, LaBRI, Bordeaux, FR: Presburger Automata
- Yevgeny Kazakov, Oxford, UK: Consequence-Based Reasoning for Description Logic Ontologies