AISB96: Report on the 3rd Workshop on Automated Reasoning
Fabio Massacci Computer Laboratory, University of Cambridge, Pembroke
Street, Cambridge CB2 3QG, England, Fabio.Massacci@cl.cam.ac.uk
Silvio Ranise Mechanized Reasoning Group - DIST, University of Genoa,
Via Opera Pia 13 - 16145 Genoa, Italy, silvio@mrg.dist.unige.it
Marco Roveri Mechanized Reasoning Group - DIST, University of Genoa,
Via Opera Pia 13 - 16145 Genoa, Italy, marco@mrg.dist.unige.it
Michael Schroeder Institut f ur Rechnergest utzte
Wissensverarbeitung, Lange Laube 3, 30159 Hannover,
schroede@kbs.uni-hannover.de
Emanuel Zarpas Computer Science departement, Ecole Nationale
Sup erieure des T el ecommunications, 46 rue Barrault 75634 Paris,
France, zarpas@inf.enst.fr
The third AISB Workshop on Automated Reasoning "Bridging the gap between
theory and practice" took place at the University of Sussex near Brighton.
It is worth noting that there has been a pleasant departure from the
traditional workshop presentation: not full papers to be presented to
a more or less sleepy audience, but rather invited speakers and panels to
facilitate the participation and warm up the discussion.
* Industry and Academia *
In the first talk J. Puget of the French enterprise ILOG presented their R D
work in constraint programming and their successful fall back in terms of
products and applications. It was encouraging to see how theoretical work is
applied and exploited to solve real-world problems such as air traffic
scheduling.
He pointed out to the audience the way corporation partners of ILOG, and more
generally suppliers of software products, spend their resources to craft a
product. Indeed, whereas 50% goes into graphics and 25% in database
management, only the remaining 25% is spent for the actual solution. And the
bulk of these 25% is related to the integration of programming languages and
tools with the rest.
The subsequent panel on ``Bridging the gap between Industry, Academia, and
Government'' chaired by C. Preist of Hewlett Packard was especially
interesting. Many of us may have noticed that in recent years applied research
and practical work became more and more important. The panel gave insight into
the reasons and opened an EC-political view of the problem.
A key observation about the shift in the policy of research funders (both at
national and EC level) was made by A. Bundy: from a horizontal model towards a
vertical model. In the past funders have tried to gather together researchers
from top centres in a horizontal fashion to boost circulations of ideas. Now a
model which includes researches (to think it out), suppliers (to work it out)
and consumers (to say it's useful) seems to take ground. As a matter of fact,
funders are concerned about wealth creation and therefore enforce an efficient
technology transfer between research and industry.
C. Priest also noted the gulf between the people doing theoretical research in
Universities and those developing products in industry. Especially because
``success'' is measured in different ways in this two environments, as pointed
out also by J. Puget in his contribution to the panel: originality and
publications are highly valued by academics and (may) lead to tenures whereas
usability and appropriate techniques are the key to success in corporate
activities. C. Priest pointed out that applied research is situated between
these opposing positions and that it should be valued as bridge between two
extremes.
* Implementing Automated Reasoning *
The panel on ``Implementing Temporal Reasoning'' chaired by M. Fisher focussed
on the issue of temporal reasoning and highlighted many of the problem facing
deduction in non classical logics. Indeed Fisher pointed out that, although
temporal reasoning has a wide range of application (specification and
verification of (concurrent) systems, temporal databases, natural language
processing etc.) it faces an exponential computational complexity,
incompleteness for the first order case and also the problem of choosing the
logics which actually matter for the particular application in the large (and
mostly unruled) family of temporal logics (an issue taken up by H.Barringer in
his invited talk later).
Different solutions to this problem were presented by the panelist. C. Dixon
presented an implementation for clausal temporal reasoning and explained the
various puzzles that must be solved for a successful implementation. Clausal
resolution has been so far one of the most successful theorem proving
techniques and tackling temporal logics within the same framework seems
actually promising.
Parallel temporal resolution was advocated by R. Johnson as a possible tool to
overcome, at least partly, the computational hardness of temporal deduction.
F. Massacci proposed a different approach based on theory approximation
(either sound or complete deduction) as a system for engineering. He pointed
out that, whereas a traditional field such analysis has an engineering
counterpart in numerical analysis, such a correspondence has to be found for
theorem proving which is still trapped with all-or-nothing computations.
The importance of approximation and empirical analysis was also noted by T.
Walsh from the audience who advertised for the ECAI workshop on Empirical
AI.
* Bridging the gap: systems and posters Presentation *
The system demonstrations served as good examples how
theoretical work is implemented and applied to practical problems. For
instance A. Sch oter of Edinburgh University presented a system called
EBL (Evidential Bilattice Logic) which has a model-based reasoning machine,
and can compute a wide class of default inferences in a polynomial time. In
this system, automated reasoning is done directly using the semantic.
M. Schroeder of University of Lisbon/Hannover presented a system to revise
contradictory logic programs and its thorough application to model-based
diagnosis and demonstrated a diagnostic process of digital circuits. It was
particularly interesting to see that theoretical results concerning the
evaluation of logic programs led to a significant speed-up for the implemented
diagnosis system.
H. Lowe of Napier University presented BARNACLE: a co-operative interface to
the CLAM inductive theorem proving system. It is
designed to maximize the synergy of the human computer partnership during
complex problem solving. It was an electronic presentation which was also used
for the poster session.
During the poster session and S. Ranise of University of
Genoa presented a methodology to extend the deduction capabilities of an
interactive theorem prover with effective and sound proof/decision procedures,
in order to enhance the theorem proving activity without compromising the
logical integrity of the prover itself.
M. Roveri (also from the University of Genoa) showed the use of abstraction in
Boolean Algebra, and the mechanisation of proofs by abstraction inside
ABSFOL (an interactive theorem prover). The approach could be used in many
applications as a tool to simplify problems.
E. Zarpas of ENST presented a proof search system for an action and causality
logic, Omega-logic, which allows to specify telecommunication protocols.
The goal is to extract correct programs from SDL specifications. Imperative
programs are synthesised from the proofs of Omega-logic sequents, obtained
from the SDL specifications themselves.
* Using Theorem Provers *
The opening of the second day of the workshop was the invited talk of H.
Barringer from Manchester University. He surveyed the fundamental concepts of
temporal logics and then focussed on Linear Discrete
Propositional Temporal Logic (LDPTL) which is a decidable characterization of
a linear temporal order. Barringer showed how LDPTL could be used in
program verification to answer questions such as ``given a program, does it
posses a certain temporal property?''. The key point is that, in general, the
program
is large, whereas the property to be proved is small. These characteristics
lead to choose model-checking in order to solve the problem by translating the
program P directly into a model representation. Still, this task must be made
computationally feasible. Many solutions were presented: restricting logic;
using encodings of models which share information, e.g. BDD based
tools such as VFORMAL; on-the-fly model-checking; local model-checking for
finite and infinite state systems and symbolic model-checking. The rationale of
Barringer's talk can be summarised by the following motto: ``Specialise or be
damned!''. In fact, logics are more expressive than programs, and therefore
modelling the properties of a program within a logic may be too expensive
because we do not need the full power of the logic (and the related
difficulties in proof search).
The panel ``Usability of Automated Reasoning Systems'' (chair H. Lowe)
investigates the degrees of usability of actual AR systems and their future
enhancements. This topic is gaining importance because we need AR systems to
be used in real application such as software and hardware verification. Many
theorems cannot be proved completely automatically, thus human intervention is
still needed and this intervention must be supported to be productive.
S. Aitken discussed how entirely automated tactics changes the way an
interactive prover can be used, because their result is either ``yes, the
formula is a theorem'' or ``no, the formula is not a theorem''. Therefore the
user is faced to an ``explanation problem'', since he/she wants to know `why'
and `where' the tactic has failed.
The fundamental differences between the paradigms of classic and constructive
logics were discussed by J. Underwood: the former is more familiar, it usually
has better decision procedures but it has less computational content; the
latter provides a unifying language for proofs and programs and it allows for
program extraction. In a similar way, if you deal with real applications then
you may need the power of a rich and flexible type system, while if you are a
novice then it is useful to start with Lego , that compels a certain
discipline in developing proofs.
A different route was taken by N. Merriam from York University: the increasing
importance of HCI in the theorem proving activity. Merriam highlights the
importance of applying software engineering techniques to develop new powerful
human interfaces to existing AR systems. These techniques are based on the
difficult merging of two worlds: the user world, where the evaluation is most
important, and the computer world, where execution is one of the implementor's
main task.
* The Way Forward *
In the Open Forum session I. Gent steered the participants through many
challenging questions posed by the audience itself such as: ``Are we just
talking to ourselves?'', ``Does Theory matter?'' etc.
A final question on which many from the audience ``tried their hands'' was
about the most promising application area for A.R. and the most exciting one.
By acclamation hw/sw verification, information retrieval, intelligent agents
for the Internet, new mathematical discoveries, HCI and education listed at
the top. However, someone pointed out that the most promising may not
be the most exciting Moreover two breakthroughs were emphasised:
focus on specialisation and tractable reasoning (see for example the
increasing importance of decidable fragments of temporal logics).
If there is a signal message from the workshop it is that there still is a gap
between theory and practice, but that many are already successfully bridging
the gap. As a final conclusion the workshop was organised very well and the
technical organisation from Sussex University was rather cute. The organiser,
Ian Gent, and AISB deserves a lot of credit for running such a useful and
enjoyable event.