(Apologies if you receive multiple copies.) ------------------------------------------------------------------------------- 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 Second Call for Papers ------------------------------------------------------------------------------- for a web version of this CFP, see: http://www.cs.chalmers.se/~ahrendt/ijcar-ws-disproving/ ------------------------------------------------------------------------------- Submission deadline extended to: April 21, 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/). (In case you do not want to use LaTeX, please contact Peter Baumgartner.) For submitting your paper, please go to the electronic submission page for Disproving 2004 (http://rpc25.cs.man.ac.uk/Disproving-04/submit/submission.cgi). The deadline for submission is extended to April 21, 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@cs.chalmers.se Peter Baumgartner MPI fuer Informatik, Saarbruecken, Germany Email: baumgart@mpi-sb.mpg.de Hans de Nivelle MPI fuer Informatik, Saarbruecken, Germany Email: nivelle@mpi-sb.mpg.de Important Dates April 18: Paper submissions deadline May 16: Notification of acceptance June 6: Final versions due Monday, July 5: new workshop date 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.