AISB96: Report on the 3rd Workshop on Automated Reasoning

Fabio Massacci^{∗}  Silvio Ranise^{†}  Marco Roveri^{‡}
Michael Schroeder^{§}  Emanuel Zarpas^{¶}

April 1996

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

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

∗Computer Laboratory, University of Cambridge, Pembroke Street, Cambridge CB2 3QG, England, Fabio.Massacci@cl.cam.ac.uk

†Mechanized Reasoning Group - DIST, University of Genoa, Via Opera Pia 13 - 16145 Genoa, Italy, silvio@mrg.dist.unige.it

‡Mechanized Reasoning Group - DIST, University of Genoa, Via Opera Pia 13 - 16145 Genoa, Italy, marco@mrg.dist.unige.it

§Institut für Rechnergestützte Wissensverarbeitung, Lange Laube 3, 30159 Hannover, schroede@kbs.uni-hannover.de

¶Computer Science departement, Ecole Nationale Supérieure des Télécommunications, 46 rue Barrault 75634 Paris, France, zarpas@inf.enst.fr

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.

2 Implementing Automated Reasoning

The system demonstrations presented afterwards served as good examples how theoretical work is implemented and applied to practical problems. For instance A. Schöter 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 (Bundy et al, 1990) inductive theorem proving system. It is designed to maximize the synergy of the human computer partnership during complex problem solving.

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 aslo noted by T. Walsh from the audience who advertised for the ECAI workshop on Empirical AI.

During the poster session 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.

H. Lowe of Napier University presented BARNACLE a co-operative theorem proving system for System developement.

3 Using Theorem Proving…

The opening of the second day of the workshop was the invited talk of H. Barringer from Manchester University. He surveyed the fundamental (syntactic and semantic) concepts of temporal logics and then focussed on Linear Discrete Propositional Temporal Logic (LDPTL) which is a decidable characterisation of a linear temporal order. Then 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?”. In fact, there is a natural encoding of the semantics of a program as a temporal formula so program verification can be reduced to entailment in temporal logic. 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 and thus avoiding to find a corresponding formula. Still, this task must be made computationally feasible. Many solutions were presented: restricting logic, e.g. use Computation Tree Logic (model-checking is polynomial in the size of formulae); use encodings of models which share information, e.g. BDD based tools such as VFORMAL (used to perform hw-verification for a synchronous subset of VHDL); on-the-fly model-checking (i.e. using hashing to determine whether a state has been visited); 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.

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