IJCAR 2004 Workshop W1

Workshop on Disproving -
Non-Theorems, Non-Validity, Non-Provability

University College Cork,
Cork, Ireland
Workshop date changed to Monday, July 5, 2004


[ Text Version of the CFP ]

Quick links:
[ Background, Scope, Topics, Workshop Goal, Audience  |  Invited Speakers  |  Venue  |  Technical Programme  |  Proceedings and Abstracts  |  Program Committee  |  Publication  |  Workshop Venue  |  Registration  |  Workshop Organisers  |  Important Dates  |  Links ]


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.


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.


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.

Invited Speakers

Alan Bundy, University of Edinburgh, Scotland.
Toby Walsh, University College Cork, Ireland.


The workshop takes place in room Boole 4 (LL2).

Technical Programme

Proceedings and Abstracts

Program Committee

Wolfgang Ahrendt (Organiser)
Peter Baumgartner (Organiser)
Christian Fermüller
Ulrich Furbach
Bernhard Gramlich
Deepak Kapur
Bill McCune
Hans de Nivelle (Organiser)
Renate Schmidt
Carsten Schürmann
Graham Steel
Cesare Tinelli
Andrei Voronkov


The final versions of all the accepted papers will be collected in a volume to be distributed at the workshop and made accessible on the web.

Beside these informal proceedings, selected papers will be published within the ENTCS (Electronic Notes in Theoretical Computer Science) series. The selection status of the individual papers was communicated to the respective authors by e-mail.

The final version should be sent by June 8th (two days after the originally announced date) to Peter Baumgartner baumgart@mpi-sb.mpg.de, both as LaTeX source and as PDF.

To format the final version, please follow the the formatting instructions. (The file prentcsmacro.sty mentioned there will be available soon).
Note that there are different instructions for ENTCS resp. 'informal proceedings only'. Of course, authors of ENTCS papers only have to send a ENTCS compatible version.

For ENTCS publications there is a *lower* bound of 10 pages. Longer papers are encouraged.

Workshop Venue

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


For registration, please use the IJCAR 2004 registration form.
Early registration ends at May 21st.

Workshop Organisation

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

Peter Baumgartner
MPI für Informatik, Saarbrücken, Germany
Email: baumgart@mpi-sb.mpg.de

Hans de Nivelle
MPI für Informatik, Saarbrücken, Germany
Email: nivelle@mpi-sb.mpg.de

Important Dates

April 21, extended Paper submissions deadline
May 16, Notification of acceptance
May 21, early registration deadline
June 8, Final versions due
Monday, July 5, new workshop date


For further information on the workshop, please contact one of the organisers.

Last modified: Tue Jun 29 14:52:38 CEST 2004