Email Gateway (Aug 17 2022 at 14:46): Email Gateway (Aug 17 2022 at 14:46):From: Wolfgang Ahrendt <ahrendt@cs.chalmers.se>
IJCAR 2006 Workshop on
DISPROVING
Non-Theorems, Non-Validity, Non-Provability
in connection with
FLoC 2006
Seattle, Washington,
August 16, 2006
DISPROVING is scheduled
right after LICS, RTA, SAT, and
right before IJCAR, CAV, ICLP,
so you can combine it with
any FLoC conference nicely.
Web Page:
www.cs.chalmers.se/~ahrendt/FLoC06-ws-disproving/
Seccond Call for Papers
=======================
Background
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, and failed-proof analysis.
Topics of relevance to the workshop therefore include
* disproving conjectures in general,
* extending standard proving methods with disproving capabilities,
* approximate 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 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.
Technical Programme
The technical program will include presentations of the accepted
papers, discussions about the state and future of the field, and two
invited talks.
Programme 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
Invited Speaker
* Silvio Ranise, LORIA/INRIA-Lorraine.
* Jian Zhang, Institute of Software, Chinese Academy of Sciences.
Submission
Submissions should not exceed 10 pages.
Please use the electronic submission page at:
www.easychair.org/DISPROVING06/
The submission procedure is electronic only, and only PDF files are
acceptable.
The deadline for submission is 26th of May 2006.
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.
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 Venue
The workshop will be held on August 16 as part of
FLoC 2006 (Federated Logic Conference),
The Seattle Sheraton Hotel and Towers,
Seattle,
Washington,
August 10 - 22, 2006
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
Important Dates
May 26: paper submissions deadline
new: June 21: notification of acceptance
new: July 05: final version due
Wednesday, August 16: workshop date
Links
* Workshop web page: www.cs.chalmers.se/~ahrendt/FLoC06-ws-disproving/
* IJCAR 2006 home page: ijcar06.uni-koblenz.de/
* FLoC 2006 home page: research.microsoft.com/floc06/
* last year's workshop web page:
www.cs.chalmers.se/~ahrendt/cade20-ws-disproving/
For further information on the workshop, please contact any of the
organizers.
Last updated: Nov 21 2024 at 12:39 UTC