Overview

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.

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.

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.

Program

• DISPROVING program
• DISPROVING accepted papers
• DISPROVING pre-proceedings

Invited Talks

• Wednesday, August 16th, 09:00‑10:00
  Jian Zhang (Institute of Software, Chinese Academy of Sciences)
  Model and Counterexample Search: Successes and Challenges [pdf]
• Wednesday, August 16th, 14:00‑15:00
  Silvio Ranise (LORIA-INRIA-Lorraine & Università degli Studi di Milano)
  Satisfiability Solving for Program Verification: towards the efficient combination of Automated Theorem Provers and Satisfiability Modulo Theory Tools [pdf]

Publication

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

The organizers aim for properly published 'post-workshop' proceedings, probably in the form of a journal special issue. They will be 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 the 2004 workshop on DISPROVING appeared within ENTCS.)

Workshop Organizers

• Wolfgang Ahrendt, Chalmers University of Technology, Göteborg, Sweden, Email: ahrendt AT cs.chalmers.se
• Peter Baumgartner, National ICT Australia, Logic and Computation Program, Canberra, Australia, Email: Peter DOT Baumgartner AT nicta.com.au
• Hans de Nivelle, MPI für Informatik, Saarbrücken, Germany, Email: nivelle AT mpi-sb.mpg.de

Program Committee

• Wolfgang Ahrendt (Organizer)
• Peter Baumgartner (Organizer)
• Johan Bos
• Simon Colton
• Christian Fermüller
• Bernhard Gramlich
• Bill McCune
• Hans de Nivelle (Organizer)
• Michael Norrish
• Renate Schmidt
• Carsten Schürmann
• John Slaney
• Graham Steel
• Cesare Tinelli
• Calogero Zarba