[DL] IJCAR Workshop on Disproving

Thu Jan 29 17:17:05 CET 2004

(Apologies if you receive multiple copies.)

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

                              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 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, 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
examples for non-theorems. This workshop should contribute to the
forming of a disproving community within AR, and give according work 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 the ones sometimes 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 to be presented.

Technical Program

The technical program will include presentations of the accepted
papers as well as an invited talk.

Invited Speaker

  * Alan Bundy, University of Edinburgh

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

Submission

Submissions should not exceed 10 pages. Please use LaTeX, with the
header specified at the IJCAR workshops web page
(www.mpi-sb.mpg.de/~baumgart/ijcar-workshops/).  The submission
procedure will be electronical only.  Details will be announced in
due time on the workshop web page.

The deadline for submission is April 18, 2004.

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.

Depending on the number and quality of the submissions, the organizers
plan for properly published post proceedings, 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.

Workshop Venue

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

Workshop Organizers

    Wolfgang Ahrendt
    Chalmers University of Technology, Gothenburgh, Sweden
    Email: ahrendt 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

Important Dates

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

Links

  * Workshop web page: www.cs.chalmers.se/~ahrendt/ijcar-ws-disproving/
  * IJCAR 2004 workshops page: 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.