| Alessandro Cimatti, IRST, Trento, (shared with CFV and VERIFY) |
|---|---|
|
| Koen Claessen, Chalmers University of Technology, Göteborg, (abstract) |
|
| Cesare Tinelli, University of Iowa, (shared with CFV and VERIFY) (abstract) |
CADE 2007Workshop
|
Alessandro Cimatti, IRST, Trento, (shared with CFV and VERIFY) Koen Claessen, Chalmers University of Technology, Göteborg, (abstract) Cesare Tinelli, University of Iowa, (shared with CFV and VERIFY) (abstract)
| 09:00 - 11:00 |
1st Session: joint with CFV and VERIFY |
| 09:00 - 10:00 |
Invited Talk Cesare Tinelli Trends and Challenges in Satisfiability Modulo Theories |
| 10:00 - 11:00 |
Invited Talk Alessandro Cimatti Satisfiability Modulo the Theory of Bit Vectors |
| 11:00 -
11:30 |
Break |
| 11:30 - 12:30 |
2nd Session: joint with VERIFY |
| 11:30 - 12:00 | Alan Bundy Where's My Stuff? An Ontology Repair Plan (DISPROVING Talk) |
| 12:00 - 12:30 | Philipp Rümmer A Sequent Calculus for Integer Arithmetic with Counterexample Generation (VERIFY Talk) |
| 12:30 - 14:00 |
Lunch |
| 14:00 - 15:30 |
3rd Session |
| 14:00 - 15:00 |
Invited Talk Koen Claessen A Paradigm Shift in ATP: Towards Model-based Reasoning Systems |
| 15:00 - 15:30 | Jan Otop Solution to some right alternative ring problems |
| 15:30 - 16:00 |
Break |
| 16:00 - 17:30 |
4th Session |
| 16:00 - 16:30 | Didier Galmiche, Dominique Larchey-Wendling and Yakoub Salhi Provability and Countermodels in Gödel-Dummett Logics |
| 16:30 - 17:00 | Arjeh M. Cohen, Jan Willem
Knopper, and Scott H. Murray Automatic Proof of Graph Nonisomorphism |
| 17:00 - 17:30 | Hans de Nivelle Redundancy for Geometric Resolution |
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.
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, 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.
This the 4th DISPROVING workshop, following the workshops at IJCAR 2004, CADE 2005, and FLoC 2006.
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.
Beside mature work, we also solicit preliminary work or work in progress to be presented.
Wolfgang Ahrendt (Co-Chair) Franz Baader Peter Baumgartner (Co-Chair) Simon Colton Christian Fermüller Bernhard Gramlich William McCune Hans de Nivelle (Co-Chair) Michael Norrish Silvio Ranise Renate Schmidt Carsten Schürmann Graham Steel
Submissions should not exceed 10 pages.
Submission will be electronic only, using EasyChair. Here is the electronic submission page .
The deadline for submission is 25th of May 2007.
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.
Together with the organisers of the VERIFY'07 workshop at CADE, we are planing a joint journal special issue on the topics of both workshops. Authors of papers presented at DISPROVING and VERIFY will be welcome to submit extended and revised versions of their papers. However, contributions will not be limited to those based on papers presented at either workshops; other submission are welcome as well.
The workshop will be held on July 16, as part of
CADE 2007
(Conference on Automated Deduction),
International University Bremen,
Germany,
July 17 - 20, 2007
Wolfgang Ahrendt
Chalmers University of Technology, Göteborg, Sweden
Email: ahrendt AT chalmers.sePeter Baumgartner
National ICT Australia, Logic and Computation Program, Canberra, Australia
Email: Peter DOT Baumgartner AT nicta.com.auHans de Nivelle
Institute for Computer Science, University of Wroclaw, Poland
Email: nivelle AT ii.uni.wroc.pl
May 25: paper submissions deadline
June 12: notification of acceptance
June 22: final version due
Monday, July 16: workshop date
For further information on the workshop, please contact any of the organisers.