Report on the FOURTH WORKSHOP ON AUTOMATED REASONING
----------------------------------------------------
[ held as part of the AISB Workshop Series, April 1997, Manchester, UK ]
INTRODUCTION
------------
The 1997 Automated Reasoning Workshop was the fourth in the now well
established series of workshops on Automated Reasoning held in
association with AISB. As in previous years, it was organised mainly
as a set of panel sessions, the aim being to stimulate discussion and
to promote a true workshop atmosphere. In addition we were fortunate to
have a number of distinguished invited speakers, particularly Jeff
Paris (Victoria University of Manchester) and Ray Reiter (University
of Toronto).
The workshop was organised by a committee chaired by Michael Fisher
(Manchester Metropolitan University), and financial support was
provided by the AISB, the Manchester Metropolitan University, and the
Compulog network, whose generous sponsorship enabled us to invite Ray
Reiter.
INVITED PRESENTATIONS
---------------------
The invited speakers provided the following presentations:
"Use of Maths in AI" - Jeff Paris
"Modeling Dynamical Systems in the Situation Calculus: Some
Representational and Computational Issues for Automated
Reasoning" - Ray Reiter
The first talk was a plenary presentation, being shared by all the
AISB workshops. Professor Paris described his own work on modelling
belief, in particular his use of a "maximum entropy function" for
producing an agent's beliefs from its knowledge.
In the second talk, introduced and reviewed by Tony Cohn (Leeds
University), Professor Reiter described the use of Situation Calculus
in his "Cognitive Robotics" work. He showed how the Situation
Calculus, suitably extended, can be effective in modelling the actions
and effects of robotic agents, and described how an agent's behaviour
can be animated by directly executing the Situation Calculus formulae,
an approach taken in the GOLOG programming language. In manipulating
agent descriptions, a form of automated reasoning is required although
the restricted form considered requires only rewriting using
equivalences.
A third invited talk was planned, this time by Ulrich Furbach on
"Theorem Proving and Logic Programming". Unfortunately, Professor
Furbach suffered an accident immediately before the workshop and was
unable to attend. The slot scheduled for this talk was filled by a
combination of an overview of the COMPULOG Area on Automated Deduction
Systems (http://www.cs.bham.ac.uk/~mmk/compulog/meeting4.97.html),
presented by Manfred Kerber (Birmingham University), an additional
presentation on "Automated Deduction and Rough Information", presented
by Laurent Vigneron (Nancy), and a report on the work of the Computer
Science Research Strategy Group both in general and with respect to
Automated Reasoning
(http://www.dcs.gla.ac.uk/research/uk-cs-research/), presented by Alan
Bundy (University of Edinburgh).
PANEL SESSIONS
--------------
Panel A: "Bridging the Gap between the AI Reasoning and the Automated
Deduction Communities "
Chair: Alan Frisch (University of York)
Panelists: Alan Bundy (University of Edinburgh); Ian Gent (Strathclyde
University), Hans Juergen Ohlbach (Imperial College),
Ray Reiter, Lincoln Wallen (Oxford University)
Alan Frisch opened the panel by pointing out that the field of
automated reasoning comprises two distinct communities: the AI
reasoning community centred around the International Conference on
Principles of Knowledge Representation and Reasoning (KR) and the
automated deduction community centred around the International
Conference on Automated Deduction (CADE). He sensed that the interests
of the present workshop series were narrowing to a point similar to
that of CADE and pleaded for the series to maintain its original goal,
as stated in the workshop's call for papers, of bringing together a
diversity of researchers.
Alan Frisch claimed that the AI reasoning/automated deduction
distinction was not merely a social one but also one of research topic
and methodology. His survey of KR and CADE publications showed that a
majority of KR papers are concerned substantially with representation
issues, whereas only a small percentage of CADE papers are.
Furthermore, a large number of KR papers address the question of what
behaviour a reasoning system should exhibit, whereas only one CADE'94
paper does.
Alan Bundy continued this theme by discussing the role of knowledge
representation in automated reasoning. He claimed that in automated
mathematics the representation is given and the logic is standard,
whereas in formal methods the logics vary and, in automated commonsense
reasoning, representation is a research issue. However,
in automated mathematics serious representation issues emerge at the
meta-level in representing and reasoning about proof search.
Lincoln Wallen argued that commonsense reasoning as well as
non-deductive reasoning was needed for automated theorem proving. He
also argued that the field of knowledge representation has reached the
point where it needs to evaluate its formalisms with respect to their
contribution to systemic behaviour. Formalisms used by reasoning
systems, as distinct from those used for analysis, need to be simple.
Ray Reiter further elaborated the claim that commonsense reasoning
must be simple and "shallow". His experience has led him to conclude
that the analysis of complex non-monotonic formalisms can result in
simple "closed forms," the most common of which is a database with a
set of definitions.
Hans Juergen Ohlbach discussed his experience in building an automated
reasoning service for a natural language processing system. This
system was also structured as a database with a hierarchy of
definitions. Although the system had implemented modal logics of
knowledge and belief, it turned out that the logical properties of
these operators frequently addressed in the literature where not
needed at all. What was actually needed to build an agent's belief
set was essentially heuristical and outside the scope of such logics.
Ian Gent urged for increased communication between the two
communities. He used his research area, propositional satisfiability,
to illustrate the harmful effect of insufficient communication.
These presentations were followed by a wide-ranging open discussion
whose dominant topic was the role of representation in mathematical
reasoning. It was noted that the successful use of automated theorem
provers in solving open mathematical problems has been
predominantly--perhaps exclusively--in areas, such as group theory,
where problems are essentially formal. But even here, success has
often required human expertise to properly configure the automated
system. Hence, OTTER, a system that accommodates substantial
configuration has been among the most successful. It was observed
that formulating a problem is a crucial task that requires a great
deal of skill. The mapping of Euclidean geometry to analytic geometry
is an example of a case where a well-suited problem formulation has
led to great progress in automation. The formalisation of inference
rules for partial functions was given as an example of an area where
progress was still needed. There appeared to be wide agreement that
the representation problem for mathematics was far from solved.
Panel B: "The Future of Automated Reasoning Research"
Chair: Alan Bundy (University of Edinburgh)
Panelists: Rob Arthan (Lemma 1); Dominic Semple (EPSRC); Lincoln
Wallen (Oxford University).
Lincoln Wallen emphasised the growing importance of computer science
practitioners being skilled professionals. Rob Arthan discussed the
role of automated reasoning systems in formal development of
high-assurance systems. Although there has been a lot of progress in
the last decade or so, there is still a great deal of work left to do
before the potential of mechanized proof is realised in practice.
Much of what is needed is consolidation -- not so much building
bridges as filling in the ravines that the pioneers have already
bridged. Dominic discussed the new structure of EPSRC and the
continued support within it for basic and theoretical
research. However, grant applicants must ensure they address the needs
of the "users" of their research. These users could be fellow
academics. Automated reasoning research is well supported by
EPSRC. There are no figures for AR per se, but Theoretical Computer
Science takes about 30% of Dominic's budget and AI about 25%.
Panel C: "Can Formal Methods Flourish without Automated Reasoning?"
Chair: Ursula Martin (University of St. Andrews)
Panelists: Rob Arthan (Lemma 1); Helen Lowe (Napier University);
Harrie de Swaart (Tilburg University); Konrad Slind
(Cambridge University).
A range of issues was discussed. A related question was whether formal
methods can flourish: it had been oversold in the past, but was now
emerging as a key component of specialised areas such as safety
critical systems and hardware designs, with Z emerging as the industry
standard.
Arguments for the proposition included the increasing interest in
"light formal methods": using formal specification without formal
proof support as a means of clarifying system requirements and design
at an early stage, and the difficulty of using many automated tools
which meant that many of the most impressive work was obtained by
highly skilled users using interactive systems.
Arguments against the proposition included the importance of
mechanically verified formal proof or what was the point of formal
methods at all, particularly for the verification of complicated
designs where it was impossible to rely on hand or informal proof, and
the importance of increasing the automation of such proofs so that
tools could be used with confidence by non-expert users.
Panel D: "How `Intelligent' should Reasoning Systems be?" Chair:
Michael Fisher (Manchester Metropolitan University)
Panelists: Andrew Adams (University of St. Andrews); Andrew Ireland
(Heriot-Watt University); Manfred Kerber (Birmingham
University); Judith Underwood (Glasgow).
Given that ("fast but dumb") systems such as Otter have had such
notable successes, for example results in Algebra, how `intelligent'
should we attempt to make our automated reasoning systems?
Most of the panelists felt that considerable `intelligence' was
required within theorem-provers. In particular Andrew Ireland listed
areas in which he saw proof planning as being essential, for example
problems characterising huge search spaces, and where there was a need
for user interaction. Judith Underwood argued that there were two
different application areas for Automated Reasoning techniques, one
where fast theorem-provers such as Otter were required, the other
where a deeper understanding of the problem space is required. Manfred
Kerber argued that, for our provers to be effective, then we would
have to solve, at least partially the general AI problem. He suggested
a study of Polya's work in order to characterise what kind of
intelligence needed to be added to theorem provers.
In the discussion session following the presentations, Alan Bundy
defended the proof planning view. In addition, he claimed that the
Otter proof of the Robbins conjecture had required a large amount of
human pre-processing as well as a significant element of trial and
error (i.e. tinkering with parameters until proof ran quickly).
Michael Fisher agreed, but suggested that Otter's success pointed to
the importance of a fast underlying prover, together with an
appropriate representation of the problem, rather than any degree of
planning within the prover itself. He agreed with Manfred Kerber's
view that in trying to prove very complex theorems, we are essentially
attacking the AI problem, and drew a parallel between this debate and
the cognitive/behavioural conflict in Robotics.
FUTURE
------
The Fifth workshop in this series will be held at the University of
St. Andrews at the end of March 1998. The workshop will be chaired by
Ursula Martin, and will be co-located with, and immediately prior, to
the Fourteenth British Colloquium for Theoretical Computer
Science. The two events will share several sessions and combined
registration.
WWW
---
Details of all these workshops can be found at
http://www.cs.york.ac.uk/~frisch/AutoReason