[TYPES] IJCAR 2004 Workshop W1 on Disproving

[Hans de Nivelle]

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

                      IJCAR 2004 Workshop W1                             
                                                                               
                     Workshop on Disproving -         
           Non-Theorems, Non-Validity, Non-Provability

                     University College Cork,
                         Cork, Ireland
                      Sunday, July 4, 2004
     
                                                                          
                         Call for Papers                                

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

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

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

Submission deadline: April 18, 2004


Background

Automated Reasoning (AR) traditionally has focused on proving
theorems. Correspondingly, 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 can be called 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 could be for example 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, and others.

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,
  * repairing non-theorems.

Workshop Goal

The workshop will provide a platform for the exchange of ideas between
researchers concerned with disproving or related issues. 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
benchmark examples for non-theorems. This workshop should contribute 
to the forming of a disproving community within AR, and give work in
this field a greater visibility.
We aim at researchers from all areas of automated reasoning. 
The areas include (but are not restricted to) first-order theorem
proving, inductive theorem proving, rewriting based reasoning,
higher-order theorem proving, logical frameworks, and special purpose
logics like the ones used for software verification systems
(dynamic logic, Hoare logic). We also target at the model generation
community.
Beside mature work, we also solicit preliminary work or work in
progress.



Program Committee

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


Organizers

    Wolfgang Ahrendt,
    Chalmers University of Technology, Gothenburgh, Sweden
    Email: ahrend at cs.chalmers.se

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

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


Details

- Submissions should not exceed 10 pages. Submission will be electronic
  through the workshop homepage.
  (www.cs.chalmers.se/~ahrendt/ijcar-ws-disproving/) 
  Please prepare the submission (ps or pdf) using LaTeX, with the
  header given at the workshop homepage. 

- Deadline for submission is April 18, 2004.
- The final versions of the selected contributions will be collected in
  a volume distributed at the workshop and made accessible on the web.

  Depending on the number and quality of the submissions, the 
  organizers plan for properly published post proceedings, containing
  extended versions of selected workshop papers, but also open to 
  non-participants, in all cases with fresh reviewing. The decision 
  about this will be taken at or shortly after the workshop.

- The workshop will be held on July 4th as part of IJCAR 2004
  (2nd International Joint Conference on Automated Reasoning),
  Cork, Ireland, July 4 - July 8, 2004.

- The technical program will include presentations of the accepted
  papers as well as an invited talk by Alan Bundy, University of
  Edinburgh. 

Important Dates

    April 18:  Paper submissions deadline
    May   16:  Notification of acceptance
    June   6:  Final versions due
    July   4:  Worskhop


Links

  * Workshop homepage: www.cs.chalmers.se/~ahrendt/ijcar-ws-disproving/
  * IJCAR 2004 workshops: www.mpi-sb.mpg.de/~baumgart/ijcar-workshops/
  * IJCAR 2004 home page: www.4c.ucc.ie/ijcar/

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