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


Erden in AI roundtab...

On Friday 4th September, philosopher and AISB member Dr Yasemin J Erden, participated in an AI roundtable at Second Home, hosted by Index Ventures and SwiftKey.   Joining her on the panel were colleagues from academia and indu...


AISB Convention 2016

The AISB Convention is an annual conference covering the range of AI and Cognitive Science, organised by the Society for the Study of Artificial Intelligence and Simulation of Behaviour. The 2016 Convention will be held at the Uni...


Bishop and AI news

Stephen Hawking thinks computers may surpass human intelligence and take over the world. This view is based on the ideology that all aspects of human mentality will eventually be realised by a program running on a suitable compu...


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


Al-Rifaie on BBC

AISB Committee member and Research Fellow at Goldsmiths, University of London, Dr Mohammad Majid al-Rifaie was interviewed by the BBC (in Farsi) along with his colleague Mohammad Ali Javaheri Javid on the 6 November 2014. He was a...


AISB YouTube Channel

The AISB has launched a YouTube channel: http://www.youtube.com/user/AISBTube (http://www.youtube.com/user/AISBTube). The channel currently holds a number of videos from the AISB 2010 Convention. Videos include the AISB round t...



AISB event Bulletin Item

CALL FOR PARTICIPATION: Tutorial on Applying Mechanised Reasoning in Economics Making Reasoners Applicable, 17 Sep 2013, Koblenz, GERMANY



Our audience comprises computer scientists developing or using
mechanised reasoning systems, or interested in learning how to use them.
The message of this tutorial is:

1. There are interesting nails (problems) out there in economics,
waiting for hammers (tools) from computer science to be applied to them.
2. Those domain experts who have the interesting problems do not speak
the same language as computer scientists do.
3. Therefore, it takes some effort to make computer science tools
applicable in such domains:
   * giving meaningful feedback on errors,
   * writing application-oriented documentation,
   * trying hard to support users who understand textbook mathematics
but not proof calculi, etc.


We have a vision of increasing confidence in economics' models and
mechanisms. Auction designs are under constant evolution as they seek to
incorporate lessons learned and to recognise specific features of the
markets in which they are run. Similarly, current models for financial
risk measurement are too large and change too quickly to be checked by
hand. These challenges affect not only the economics sector itself, but
also the government as it regulates the economy, and thus the general
public. Since the software used is mission critical it should be
verified to a high level of reliability.

We believe that such problems can be addressed by representing the
underlying knowledge in a formal, explicit way that is accessible to
mechanised reasoning tools. These have already been applied to
economics, albeit by computer scientists rather than the economists

Many economists have postgraduate training in mathematics; historically,
it has been less common for them to have training in computer science.
Therefore, despite a growing interface (consider, e.g., the ACM
Transactions on Economics and Computation), they lack awareness of the
existence of reasoning tools and their appropriateness for tasks in
economics. Moreover such tools are still challenging to use. The
objective of our ForMaRE project (formal mathematical reasoning in
economics) is to raise awareness and to enable economists to work with
the languages and tools of their choice.

RESEARCH CONTEXT (Computer Science Perspective)

How can we make formal methods familiar to economists? Concretely, we
are developing a basic Auction Theory Toolbox of formalisations, on top
of which auction designers can formalise and verify their own auction
designs, and we are getting started with applying similar techniques to
matching markets and financial risk management. This tutorial reports on
our experience and insights from carrying out this research.

>From a computer science perspective, our toolbox building approach

1. identifying the right language to formalise the theory (i.e. being
sufficiently expressive while still supporting efficient proofs), and
2. identifying a a mechanised reasoning system whose input and output
are comprehensible to economists, who usually do pen-and-paper proofs
and are familiar with mathematical textbook notation.

We have so far gained experience with the languages/systems Isabelle/HOL
and its jEdit IDE, Theorema, CASL and its Hets IDE and the System on
TPTP web service, Mizar, as well as Prover9 and Mace4.

* Economists may find it appealing that the structure of an Isabelle or
Mizar proof resembles the structure of a paper proof, that Theorema is
an add-on to the familiar Mathematica CAS with its textbook-like
notebook interface, or that Hets allows for uniformly feeding one
formalisation into a wide range of highly efficient automated theorem
* It may deter them that little documentation for these tools is
available, or that it requires strong background knowledge, and that the
investigation of unsuccessful automated proof attempts requires a good
understanding of the underlying calculus.


The last part of the tutorial involves an interactive matchmaking
session. We will try to match tutorial participants who are developers
or experienced users of tools (if you are, please contact us in
advance!) and economics problems to which consider these tools may be
applicable. We will briefly present the respective problem and ask the
respective participant for a brief voluntary presentation of his or her
tool. From our connections in the economics community (cf. our research
collaborators and our organisation of the AISB 2013 symposium on
Enabling Domain Experts to use Formalised Reasoning) we have a portfolio
of around a dozen potentially matching problems.


* Christoph Lange, Computer Science, University of Birmingham, UK
* Manfred Kerber, Computer Science, University of Birmingham, UK
* Colin Rowat, Economics, University of Birmingham, UK

Please contact us at formare-management@cs.bham.ac.uk.