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 al-Rifaie ( Tu...


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


Computerised Minds. ...

A video sponsored by the society discusses Searle's Chinese Room Argument (CRA) and the heated debates surrounding it. In this video, which is accessible to the general public and those with interest in AI, Olly's Philosophy Tube ...


Connection Science

All individual members of The Society for the Study of Artificial Intelligence and Simulation of Behaviour have a personal subscription to the Taylor Francis journal Connection Science as part of their membership. How to Acce...



AISB event Bulletin Item

Automated Reasoning Workshop 2007 - Call for participation

Automated Reasoning Workshop

19th - 20th April 2007

Department of Computing, Imperial College, London


The 2007 automated reasoning workshop is the latest in a long series
of successful workshops which aim to provide an informal forum for the
automated reasoning community to discuss recent work, new ideas and
current trends. It aims to bring together researchers from all areas
of automated reasoning in order to foster links and facilitate
cross-fertilisation of ideas among researchers from various
disciplines; among researchers from academia, industry and government;
and between theoreticians and practitioners.

Please find below details of this year's workshop:


Geoff Sutcliffe, University of Miami
Alice Miller, University of Glasgow

Abstract for Geoff's talk:

This talk describes the design, implementation, and testing of a
system for selecting necessary axioms from a large set also containing
superfluous axioms, to obtain a proof of a conjecture. The selection
is determined by semantics of the axioms and conjecture, ordered
heuristically by a syntactic relevance measure. The system is able to
solve many problems that cannot be solved alone by the underlying
automated reasoning system.

Abstract for Alice's talk:

Model checking is an established technique for checking the
reliability of software-controlled systems and constitutes one of the
leading applications of logic to Computer Science. This automatic
technique involves the construction of a model of a system over which
properties are checked. One of the major problems with model checking
is the (so-called) state-space explosion problem -- where models
become too large to feasibly check. A popular technique for
combatting state-space explosion is symmetry reduction. In this talk I
introduce a variety of model checkers and give an introduction to
symmetry reduction methods, and their implementations.


We have a very broad and interesting selection of extended abstracts
which will be presented this year. Each extended abstract will be
discussed both with a short presentation and in a poster session.

Forms of factoring in paramodulation-based calculi
Vladimir Aleksic

Compressing propositional refutations using subsumption
Hasan Amjad

Proof tool integration with proof general
David Asipinall and Christoph Luth

Towards automated verification of grid component model
Alessandra Basso and Alexander Bolotov

The LEO-II Project
Christoph Benzmuller, Larry Paulson, Frank Theiss and Arnaud Fietzke

Automating Natural Deduction for Temporal Logic
Alexander Bolotov, Oleg Grigoriev and Vasilyi Shangin

A tableau compiled labelled deductive system for hybrid logic
Krysia Broda and Alessandra Russo

Towards a theory of ontology repair (or truthfulness considered harmful)
Alan Bundy

A rational reconstruction of a system for experimental mathematics
Jacques Carette, William Farmer and Volker Sorge

Cleanly combining specialised program analysers
Nathaniel Charlton and Michael Huth

Prediction using machine learned constraint satisfaction programs
John Charnley and Simon Colton

The Language EC+
Robert Craven and Marek Sergot

A common semantic basis for BDI languages
Louise Dennis, Rafael Bordini, Michael Fisher and Berndt Farwer

Tractable temporal reasoning
Clare Dixon, Michael Fisher and Boris Konev

A digital library based on Mizar
Jeremy Gow and Paul Cairns

Proof critics for IsaPlanner
Moa Johansson, Lucas Dixon and Alan Bundy

Interaction and depth against nondeterminism in proof search
Ozan Kahramanogullari

Formal verification of implementability of timing requirements
Mark Lawford, Xiayong Hu and Alan Wassung

Dynamic backtracking for modal logics
Zhen Li and Renate Schmidt

Extensions of the Knuth-Bendix ordering with LPO-like properties
Michel Ludwig

Supporting proof in a reactive development environment
Farhad Mehta

Encodings of bounded LTL model checking in effectively propositional logic
Juan Navarro-Perez and Andrei Voronkov

Using resolution to generate natural proofs
David Robinson

Analysis of blocking mechanisms for description logics
Renate Schmidt and Dmitry Tishkovsky

A universal GUI for theorem provers
Bosko Stankovic, Nenad Krdzavac and Vladan Devedzic

SRASS - a semantic relevance axiom selection system
Geoff Sutcliffe

Proving producibility of concepts
Pedro Torres and Simon Colton

Implementing tractable temporal logics
Lan Zhang, Clare Dixon and Ulrich Hustadt


Registration for the workshop has recently been opened. For details of
how to register, please see the workshop web page here:


If you have any questions about the workshop, please do not hesitate to
contact the workshop organiser: Simon Colton (