CFProposal AISB2018

  The Society for the Study of Artificial Intelligence and Simulation for Behaviour (AISB) is soliciting proposals for symposia to be held at the AISB 2018 convention.The longest running convention on Artificial Intelligence, A...


Insurance AI Analy...

Insurance AI Analytics Summit, October 9-10, London Join us for Europe’s only AI event dedicated to insurance where 300 attendees will unite from analytics, pricing, marketing, claims and underwriting. You’ll find out how advan...


AISB 2018 Convention

  The longest running convention on Artificial Intelligence, AISB 2018 will be held at the University of Liverpool, chaired by Floriana Grasso and Louise Dennis. As in the past years, AISB 2018 will provide a unique forum for p...


AI Summit London

     The AI Summit London: The World’s Number One AI Event for Business  Date: 9-10 May 2017 Venue: Business Design Centre, London. The AI Summit is the world’s first and largest/number one conference exhibition dedicated to t...


AISB Wired Health

    AISB and WIRED events have partnered to bring together inspirational high-profile speakers. Join hundreds of healthcare, pharmaceutical and technology influencers and leaders at the 4th Annual WIRED Health event, taking pl...


Hugh Gene Loebner

  The AISB were sad to learn last week of the passing of philanthropist and inventor Hugh Gene Loebner PhD, who died peacefully in his home in New York at the age of 74.  Hugh was founder and sponsor of The Loebner Prize, an an...


AI Europe 2016

  Partnership between AISB and AI Europe 2016: Next December 5th and 6th in London, AI Europe will bring together the European AI eco-system by gathering new tools and future technologies appearing in professional fields for th...


AISB convention 2017

  In the run up to AISB2017 convention (, I've asked Joanna Bryson, from the organising team, to answer few questions about the convention and what comes with it. Mohammad Majid...


Harold Cohen

Harold Cohen, tireless computer art pioneer dies at 87   Harold Cohen at the Tate (1983) Aaron image in background   Harold Cohen died at 87 in his studio on 27th April 2016 in Encintias California, USA.The first time I hear...


Dancing with Pixies?...

At TEDx Tottenham, London Mark Bishop (the former chair of the Society) demonstrates that if the ongoing EU flagship science project - the 1.6 billion dollar "Human Brain Project” - ultimately succeeds in understanding all as...



AISB event Bulletin Item

CFP: CADE 2007 Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability

CADE 2007 Workshop on

Non-Theorems, Non-Validity, Non-Provability

Bremen, Germany,
July 16, 2007

Web Page:

Call for Papers


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.

Workshop Goal

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

Programme Committee

  * Wolfgang Ahrendt (Co-Chair)
  * Franz Baader
  * Peter Baumgartner (Co-Chair)
  * Simon Colton
  * Christian Fermller
  * Bernhard Gramlich
  * William McCune
  * Hans de Nivelle (Co-Chair)
  * Michael Norrish
  * Silvio Ranise
  * Renate Schmidt
  * Carsten Schrmann
  * Graham Steel

Invited Speakers

  * Koen Claessen, Chalmers University of Technology, Gteborg
  * N.N.


Submissions should not exceed 10 pages.

Submission will be electronic only, using EasyChair. Please use the
electronic submission page which will soon be linked from here. A link
to the submission page will be added later at this point.

The deadline for submission is 11th 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

Together with the organisers of the VERIFY 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

Workshop Venue

The workshop will be held on July 16, as part of
CADE 2007 (Conference on Automated Deduction),
International University Bremen,
July 17 - 20, 2007

Workshop Organizers

    Wolfgang Ahrendt
    Chalmers University of Technology, Gteborg, Sweden
    Email: ahrendt AT

    Peter Baumgartner
    National ICT Australia, Logic and Computation Program, Canberra, Australia
    Email: Peter DOT Baumgartner AT

    Hans de Nivelle
    MPI fr Informatik, Saarbrcken, Germany
    Email: nivelle AT

Important Dates

    May 11: paper submissions deadline
    June 08: notification of acceptance
    June 22: final version due
    Monday, July 16: workshop date


   * Workshop web page:
   * CADE 2007 home page:
   * Last year's workshop web page:

For further information on the workshop, please contact any of the organisers.