\documentclass[12pt]{article}
\usepackage{a4wide}\parindent0mm
\title{\vspace*{-1cm}{\normalsize Report on the AISB-Workshop}\\
Automated Reasoning:\\ Bridging the gap between theory and practice}
\author{1.-2. April 1996}
\date{}
\begin{document}
\maketitle
This workshop was not organised as a mini-conference, but in order to
stimulate discussions among the 30-35 attendees, in form of two invited
talks, four panel discussions, a demo session, and a poster session.
Of the four panels, I only describe the first in detail, since the
arguments are of general interest, even beyond the area of automated
reasoning.
\subsection*{Invited Talk by Jean-Fran\c{c}ois Puget}
The first invited talk was given by Puget (ILOG) on the applications
of techniques for solving constraint satisfaction problems or
constraint optimisation problems. This talk was sponsored by the
COMPULOG net. Typical applications are scheduling problems of airports,
transport scenarios and time tabling problems. Since constraint
satisfaction problems are essentially equivalent to propositional
logic, the general problem is NP-complete and hence too hard for
real world cases. In order to overcome this problem, special efficient
incomplete consistency checks have been developed and successfully
used.
\subsection*{Panel: Bridging the gap}
The following panel with Chris Preist (chair), Alan Bundy, Chris
Price, Jean-Fran\c{c}ois Puget had the title: ``Bridging the gap between
industry, academia, and government''.
Bundy pointed out that in the future it will become more and more
important to have industrial collaborators in order to get grants.
Such collaborators can provide tough test examples which can be the
acid test of whether the ideas really work. In order to make contact
it is necessary to attend related conferences and to make visits.
Finding possible applications of automated reasoning often requires
imagination and flexibility. The risk of potential collaborations can
be minimised by low-risk start-ups like student projects.
Price compared the situation of nowadays scientists to that of
musicians like Bach who needed patrons for his work. In particular we
can learn from their way of getting money: we have to promise what the
patron wants, we have to deliver on the promises, we have to take the
collaborator's limitation into account, and we have to be grateful.
Puget compared the different terms on which industry and science work
have to work (products vs.\ prototypes, property vs.\ publication,
practical problems vs.\ theory, development time of less than 18
months vs.\ three years). Furthermore in a commercial product only
15\% of the total effort is devoted to the proper problem solving
facility (50\% graphics, 20\% applications, 15\% data bases).
Preist stressed that industrialists and academics must accept each
other as equal partners and compromise to help the other to succeed
(work {\em with}, not {\em for\/}). Otherwise a disaster scenario is
possible, where industrialists expect academics to the work of their
R\&D department and academics expect to get paid for what they feel
like.
The discussion was partly concerned with the question how a fast
transmission of knowledge can be achieved and how the links between
pure research, applied academic research, applied industrial research,
and product R\&D can be strengthened.
\subsection*{Panel: Temporal Reasoning}
The second panel with Michael Fisher (chair), Clare Dixon, Rob
Johnson, Fabio Massacci, and Andr\'e Trudel was devoted to
``Implementing Temporal Reasoning''. In this panel, the most
interesting question that goes beyond the direct field of temporal
reasoning was how to overcome the general all-or-nothing situations in
theorem proving.
\subsection*{Invited Talk by Howard Barringer}
In his talk Barringer presented the propositional temporal logic TDTL,
which is built up using two temporal operators, namely a binary
``unless'' operator and a unary ``next'' operator. Many other
operators can be defined in terms of ``unless'' and ``next''. For this
logic exists a decidable calculus. If the TDTL language is restricted
so that only certain combinations of temporal operators can be
combined, the computational effort for evaluating expressions is
polynomial in the size of the formula. The main applications are in
program verification for finite state programs and in natural language
processing.
\subsection*{Panel: Usability of Automated Reasoning}
In the third panel, with Helen Lowe (chair), Stuart Aitken, Judith
Underwood, and Nick Merriam, aspects of user interfaces, of automation
in interactive theorem proving, and of the advantages and
disadvantages of different logical formalisms were discussed.
\subsection*{Open Session}
In the last session, chaired by Ian Gent, who was the programme chair
of the whole workshop, everybody could hand in his/her favourite
topic. Topics were: standardising the input/output of theorem provers,
the relevance of theory for applications, and the most
promising/exciting application areas for automated reasoning in the
next decade.
\vspace{0.5cm}
\footnotesize Report by:\\
Manfred Kerber, The University of Birmingham, e-mail: M.Kerber@cs.bham.ac.uk and\\
Ian Gent, University of Strathclyde, Glasgow, e-mail: ipg@cs.strath.ac.uk
\end{document}