Logic List Mailing Archive

Workshop on DISPROVING (Tallinn, Estonia, July 2005)

CADE-20 Workshop on

DISPROVING
Non-Theorems, Non-Validity, Non-Provability

Tallinn, Estonia
Friday, July 22, 2005


Call for Papers

-------------------------------------------------------------------------------

for a web version of this CFP, see:
www.cs.chalmers.se/~ahrendt/cade20-ws-disproving/

-------------------------------------------------------------------------------

Background

Automated Reasoning (AR) traditionally has focused on proving theorems. 
Because of this, AR methods and tools in the past were mostly applied to 
formulae which were already known to be true. If on the other hand a 
formula is not a theorem, then most traditional AR methods and tools 
cannot handle this properly (i.e. they will fail, run out of resources, or 
simply not terminate). The opposite of proving, which we call disproving, 
particularly aims at identifying non-theorems, i.e. showing non-validity 
resp. non-provability, and providing some kind of proof of non-validity 
(non-provability). The proof for example could be a counter model, or an 
instantiation making the formula false.

Scope

In the scope of the workshop is every method that is able to discover 
non-theorems and, ideally, provides explanation why the formula is not a 
theorem. Possible subjects are decision procedures, model generation 
methods, reduction to SAT, formula simplification methods, abstraction 
based methods, failed-proof analysis.

Topics of relevance to the workshop therefore include

   * disproving conjectures in general,
   * extending standard proving methods with disproving capabilities,
   * approximative methods for identifying non-theorems,
   * counterexample generation,
   * counter model generation,
   * finite model generation,
   * decision procedures,
   * failure analysis,
   * reparation of non-theorems,
   * heuristics that help in identifying non-theorems,
   * applications and system descriptions.

Workshop Goal

The disproving workshops are intended as a platform for the exchange of 
ideas between researchers concerned with disproving in the broad sense. By 
discussing approaches across the different AR sub-communities, the 
workshop can identify common problems and solutions. Another goal is to 
elaborate known, and discover unknown, connections between other areas and 
disproving. Also, the meeting can enable an exchange of interesting 
examples for non-theorems. A long term goal is that the workshop series 
contributes to forming a disproving community within AR, and gives the 
work on disproving a greater visibility.

Audience

Non-theorems are an issue wherever one tries to prove statements which are 
not known to be valid in advance. Therefore, we aim at researchers from 
all areas of automated reasoning. The issue of the workshop is 
particularly relevant for all logics, calculi, and proving paradigms where 
non-validity is not covered by the (plain versions of) standard methods. 
This includes (but is not restricted to) first-order logic proving, 
inductive theorem proving, rewriting based reasoning, higher-order logic 
proving, logical frameworks, and special purpose logics like for instance 
program logics. We also target at the model generation community.

Beside mature work, we also solicit preliminary work or work in progress 
to be presented.


Technical Programme

The technical program will include presentations of the accepted papers, 
discussions about the state and future of the field, and an invited talk.


Invited Speakers

   * Byron Cook, Microsoft Research, Cambridge (shared speaker with ESCAR)

   * Juergen Giesl, RWTH Aachen


Programme Committee

   * Wolfgang Ahrendt (Organizer)
   * Peter Baumgartner (Organizer)
   * Johan Bos
   * Chris Fermueller
   * Uli Furbach
   * Bernhard Gramlich
   * Bill McCune
   * Hans de Nivelle (Organizer)
   * Renate Schmidt
   * Carsten Schuermann
   * Graham Steel
   * Cesare Tinelli
   * Andrei Voronkov
   * Calogero Zarba


Submission

Submissions should not exceed 10 pages. The submission procedure will be 
electronical only, and only PDF files are acceptable. Details will be 
announced in due time on the workshop web page.

The deadline for submission is 1st of May 2005.


Publication

The final versions of the selected contributions will be collected in a 
volume to be distributed at the workshop and accessible on the web.

The organisers plan for a special issue of the Nordic Journal of 
Computing, based on extended versions of selected workshop papers, but 
open to non-participants, in all cases with fresh reviewing. The decision 
of whether to do so will be taken after the workshop. (The according post 
proceedings of last years workshop are soon to appear within ENTCS.)


Workshop Venue

The workshop will be held on Friday, 22 July, as part of CADE-20 (20th 
International Conference on Automated Deduction) Tallinn, Estonia, 22 July 
- 27 July, 2005.


Workshop Organizers

     Wolfgang Ahrendt
     Chalmers University of Technology, Gothenburgh, Sweden
     Email: ahrendt@cs.chalmers.se

     Peter Baumgartner
     MPI fuer Informatik, Saarbruecken, Germany
     Email: baumgart@mpi-sb.mpg.de

     Hans de Nivelle
     MPI fuer Informatik, Saarbruecken, Germany
     Email: nivelle@mpi-sb.mpg.de


Important Dates

     May   1:  Paper submissions deadline
     June  1:  Notification of acceptance
     June 26:  Final versions due
     Friday, 22 July: new workshop date


Links

   * Workshop web page: www.cs.chalmers.se/~ahrendt/cade20-ws-disproving/
   * CADE-20 home page: http://deepthought.ttu.ee/it/cade/

For further information on the workshop, please contact any of the
organizers.