[DL] TABLEAUX'09 Workshop on tableaux vs automata: call for submissions
Valentin.Goranko at wits.ac.za
Tue Mar 3 11:21:00 CET 2009
Workshop on tableaux versus automata as logical decision methods
Oslo, July 6, 2009
CALL FOR SUBMISSIONS
TOPIC AND OBJECTIVE:
Terminating semantic tableaux have served for a long time as one of the practically most efficient types of decision procedures for a wide range of logical systems. On the other hand, automata-based methods for testing satisfiability and model checking for various modal and temporal logics of computations have gained very wide recognition and popularity over the past two decades, because they provide uniform, elegant, and often optimal decision procedures. Furthermore, a number of increasingly efficient automata-based tools have been implemented and used for academic and industrial purposes, and there seem to be a growing perception amongst the formal verification community that these tools are superior and preferable to the tableau-based tools. That perception, however, is not based on systematic comparative analysis, and some practical experience with well-designed tableau-based tools suggest that such perception can sometimes be misleading. Moreover, various optimization techniques, such as on-the-fly methods, draw automata-based algorithms very close to tableau-like procedures, thus strongly suggesting that tableaux and automata are closely related formalisms for deciding logical satisfiability. Yet, few formal technical results to that effect are known, and the scientific discussion on the pros and cons, similarities and differences, comparisons of applicability, efficiency, and performance between tableaux and automata has so far been rather sporadic.
The purpose of the workshop is to provide an expert forum for such discussion, to provoke and foster debate between the automata and tableaux communities, and to stimulate further research on the topic.
Submissions deadline: May 4, 2009
Notification deadline: May 25, 2009
Preliminary programme: June 5, 2009
Final programme: June 12, 2009
Workshop: July 6, 2009
Submissions for workshop talks are invited by means of extended abstracts within 5 A4 pages in PDF or PS format, using Springer LNCS style. Submissions may be based on new and original, or on already published or submitted work, but they should address the topic of the workshop.
The abstracts of the workshop talks will be included in informal proceedings. No formal proceedings are currently planned, but if the workshop attracts sufficiently many good and original contributions, a journal special issue will be organized after the event.
WORKSHOP PROGRAM COMMITTEE:
Franz Baader, TU Dresden, Germany
Stephane Demri, CNRS, Cachan, France
Valentin Goranko, Univ. of the Witwatersrand, Johannesburg, South Africa
Rajeev Gore, The Australian National Univ., Canberra, Australia
Colin Stirling, University of Edinburgh, UK
Pierre Wolper, Université de Liege, Belgium
(More PC members may join)
TABLEAUX'2009 website: http://heim.ifi.uio.no/martingi/Tableaux09
Workshop website: http://www.maths.wits.ac.za/~goranko/TableauxAutomataWorkshop/TableauxAutomataWorkshop.html
ENQUIRIES to: Valentin Goranko (Workshop organizer), goranko at maths.wits.ac.za.
<html><p><font face = "verdana" size = "0.8" color = "navy">This communication is intended for the addressee only. It is confidential. If you have received this communication in error, please notify us immediately and destroy the original message. You may not copy or disseminate this communication without the permission of the University. Only authorized signatories are competent to enter into agreements on behalf of the University and recipients are thus advised that the content of this message may not be legally binding on the University and may contain the personal views and opinions of the author, which are not necessarily the views and opinions of The University of the Witwatersrand, Johannesburg. All agreements between the University and outsiders are subject to South African Law unless the University agrees in writing to the contrary.</font></p></html>
More information about the dl