CADE-20 Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability Tallinn, Estonia Friday morning, July 22, 2005 www.cs.chalmers.se/~ahrendt/cade20-ws-disproving/ The workshops DISPROVING and ESCAR are scheduled such that you can attend both. DISPROVING fills the morning, whereas ESCAR starts in the afternoon. The only overlap in time is the shared invited talk, taking place right after lunch.

	Byron Cook, Microsoft Research, Cambridge. (last talk of the workshop, shared with the ESCAR workshop)
	Jürgen Giesl, RWTH Aachen. (first talk of the workshop)

09:00-10:00	Disproving Termination of Term Rewriting Jürgen Giesl, Invited Talk
10:00-10:30	Coffee break
10:30-11:00	Validated Construction of Congruence Closures Aaron Stump
11:00-11:30	Correction of faulty conjectures and programs extraction Moussa Demba, Francis Alexandre, and Khaled Bsaies
11:30-11:45	short break
11:45-12:15	Disproving Distributivity in Lattices Using Geometric Logic Marc Bezem
12:15-12:45	Generating Counterexamples for Java Dynamic Logic Philipp Rümmer
12:45-14:00	Lunch break
14:00-15:00	Automatic Theorem Proving for Program Verification Engines Byron Cook, Invited Talk (shared with ESCAR)

• Workshop Proceedings
  (Workshop participants will get printed proceedings.)
• Paper Abstracts

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.

	Wolfgang Ahrendt (Organiser)
	Peter Baumgartner (Organiser)
	Johan Bos
	Christian Fermüller
	Ulrich Furbach
	Bernhard Gramlich
	Bill McCune
	Hans de Nivelle (Organiser)
	Harald Rueß
	Renate Schmidt
	Carsten Schürmann
	Graham Steel
	Cesare Tinelli
	Andrei Voronkov
	Calogero Zarba

Submissions should not exceed 10 pages.

Please use the electronic submission page .

The deadline for submission has been extended to the 9th of May 2005.

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 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.)

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

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

May 9: paper submissions deadline
June 3: notification of acceptance
June 26: final versions due
Friday, July 22: workshop date

• 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 one of the organisers.