AISB Workshop Series, April 1997, Manchester, UK

Michael Fisher

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

2. 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/meeting 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).

3. 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 (University of Toronto);

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 University)

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.

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

5. WWW Page

Details of all these workshops can be found at

http://www.cs.york.ac.uk/~frisch/AutoReason

Michael Fisher

Manchester Metropolitan University

Manchester, U.K.