Report on the SSAISB Workshop "Automated Reasoning: Bridging the Gap Between Theory and Practice" Alan M. Frisch, Programme Chair \footnote{Parts of this report are edited versions of session reports written by the panel moderators and speakers who are named in the report.} Department of Computer Science University of York York Y01 5DD United Kingdom frisch@minster.york.ac.uk This aim of this workshop was to address methods of bridging the gap that separates theory from practice across the wide spectrum of topics included in the area of automated reasoning broadly construed. The workshop provided an opportunity for the automated reasoning community to meet in an informal setting to discuss recent work, new ideas, and current trends in the field of automated reasoning. This was intended to be an inclusive workshop, and it succeeded in drawing participants, both students and experienced researchers, from a wide spectrum of subareas of automated reasoning. Held in Leeds on April 11 and 12, 1994, as part of the first AISB Biennial Workshop and Tutorial Series, the workshop drew thirty participants from four countries--UK, Germany, Netherlands, and USA. The program comprised six technical sessions, two organized around an invited talk, and four organized around a panel, and a wrap-up session. Each talk session consisted of an invited talk followed by a short response from a pre-designated respondent and a moderated open discussion. Each panel session consisted of an opening statement given by the panel moderator, followed by short statements from each of the panel members, a brief period of discussion among the panel members and a moderated open discussion. This format was chosen over a "mini-conference" format in order to increase participation and interaction and to focus the discussion on a few key topics. The originating impetus for this workshop came from an organising committee (Tony Cohn, John Derrick, Pat Hill, Gyuri Lajos, and Mark Tarver) of the Centre for Theoretical Computer Science at the University of Leeds. The planning and organization of the workshop were performed by the Programme Chair, Alan Frisch (University of York), who received frequent advice from Alan Bundy (University of Edinburgh), Tony Cohn (University of Leeds), and Dov Gabbay (Imperial College). Craig MacNish (University of York) served as publicity chair and Antonis Kaniclides (University of York) provided administrative assistance. In addition to the obvious contributions of SSAISB--especially from its Chairman, Tony Cohn, and from the Series Organizers, Ann Blandford (University of Cambridge) and Hyacinth Nwana (University of Keele)--this workshop was co-sponsored by the University of Leeds Centre for Theoretical Computer Science and the University of York Intelligent Systems Group. The six technical sessions and the wrap-up session are described below in the order in which they occurred. Panel: The Role of Interaction in Automated Deduction The panel moderator, Andrew Ireland (University of Edinburgh, UK) motivated the use of proof plans as a way to facilitate proof discovery and co-operative theorem proving. The benefits of proof plans become apparent when a proof attempt fails. Andrew's research has focused upon harnessing this potential through the use of proof critics. John Derrick (University of Leeds, UK) outlined his experience with the {\sc nuprl} proof development system and its application to the specification and verification of ``Synchronous Concurrent Algorithms.'' More recently John has considered other frameworks for this work, such as special purpose proof development systems, ``proof auditing,'' and systems based upon constraint logic programming. David Duffy (University of York, UK) reviewed the induction-less induction paradigm showing its incremental development. He sees the approaches of induction-less induction and classical explicit induction as potentially complementary. David's aim is to integrate the best features of both approaches. Anton Setzer (University of Leeds, UK) provided strong representation for the theory side of the ``gap'' we are trying to bridge. He reminded us of the benefits of clear thinking, which proof theory can bring when exploring systems of logic. In particular, he emphasised its usefulness in thinking about extensions to logical systems, extensions that he believes are very often handled in an ad hoc way. Mark Tarver (University of Leeds, UK) illustrated the benefits of a hybrid-theorem-proving architecture in the context of large axiom bases (over 10,000 axioms). The hybrid solution builds upon the observation that only a few axioms are required for any particular example. This reduces the task to discovering the relevant axioms. Mark believes that the hybrid approach will reduce the need for interaction in areas where it is not a practical option. Talk: Logic Program Specialization and Approximation for Optimizing Theorem Provers This talk, by John Gallagher (University of Bristol,UK) and Andre de Waal (University of Bristol, UK), tackled the problem of optimizing a theorem prover with respect to a given theory and formula, so that relevant formulas in that theory could be proved more efficiently. Such optimizations include detecting cases where certain inference rules, or certain clauses (and contrapositives of clauses) in the theory, are useless in finding proofs; the omission of such rules and clauses reduces the search space. An approach based on general-purpose logic program analysis and transformation techniques was taken, using partial evaluation and abstract interpretation of logic programs. The talk summarised the main techniques, concentrating on the use of abstract interpretation to construct a decidable regular over-approximation of the search tree of a model elimination theorem prover with a fixed object theory and formula to be proved. The approximation was used to detect and remove infinite failed branches of the search tree. Experimental results were shown confirming that significant speed-ups could be achieved on a range of standard benchmark problems. Both the response, given by Pat Hill (University of Leeds, UK), and discussion focused on clarifying the meta-programming techniques in logic programming that should be used to write the theorem prover and represent the object theory. The suggestion was also made that optimizations for classes of theory (such as definite theories) rather than only one theory at a time, could also be achieved by this method. Another idea was that this framework could use under-approximations as well as over-approximations to make optimizations. Panel: Automating Temporal Non-Monotonic Reasoning The panel moderator, Antony Galton (University of Exeter, UK), introduced the topic by discussing some representation and reasoning problems whose solution appears to require the use of non-monotonic temporal reasoning. Craig MacNish (University of York, UK) began his presentation by referring to the "catwalk phenomenon"---if the aim is to sell clothes, why show clothes that nobody will wear? The real aim is evidently to be noticed. Craig implied that something of this kind applied to temporal non-monotonic reasoning too. John Gooday (University of Leeds, UK) also expressed dissatisfaction with existing formal approaches to temporal non-monotonic reasoning, and in particular singled out circumscription as impossible to implement efficiently in practice. Instead he proposed his own formalism, the Transition Calculus. John Bell (Queen Mary and Wesfield College, UK) advocated a model-building approach to pragmatic reasoning. This requires a dynamic model theory, in which the rules are used for building models, as opposed to the more usual kind of static model theory in which the rules are used for classifying them. Finally Bob Kowalski (Imperial College, UK) argued against the introduction of special-purpose formalisms, claiming that everything one needs to do in practice can be done using Horn clauses and standard logic-programming techniques. In the open discussion no clear consensus emerged as to whether temporal non-monotonic reasoning requires special formal techniques that go beyond the standard theorem-proving repertoire, though Bob Kowalski forcefully reiterated his belief that it was always a mistake to introduce ad hoc formalisms in this way, and that ordinary Horn-clause logic programming methods should suffice. Panel: Comparing and Evaluating Proof Calculi Reiner H\"ahnle (University of Karlsruhe, Germany), the panel moderator, presented various measures and methods for comparing proof calculi. The most important are relative proof length complexity (that is the indeterministic power of calculi), complexity of the search space, and the probabilistic analysis of the behaviour of proof procedures on the theoretical side, as well as benchmark suites and usability in real applications on the practical side. In addition to these, Bernhard Beckert (University of Karlsruhe, Germany) suggested implementational complexity as another measure, the motivation for this being the need for small, highly adaptable, transparent provers as subsystems of large verification tools. Harrie de Swart (University of Tilburg, Netherlands) presented a case study comparing two particular calculi, namely resolution and analytic tableaux. He argued that for non-classical logics the ability of tableaux to deal with non-clausal formulae is crucial. Although it was argued by several people that the relevance of theoretical comparisons between calculi is limited, Uli Furbach (University of Koblenz, Germany) argued convincingly that theoretical insights in the discrepancies and similarities of different proof procedures can be a substantial aid in designing and implementing theorem provers. Finally, Rob Johnson (Manchester Metropolitan University, UK) explained some of the difficulties in migrating theorem provers to parallel architectures. The general discussion confirmed the conjecture that existing techniques for comparing and evaluating proof calculi, although certainly helpful, are not yet sufficient to conclusively evaluate usability of the calculi, especially when several paradigms are being integrated. Talk: Wanted: A Theory of Approximation for Automated Reasoning David Page (Oxford University, UK) and Alan Frisch (University of York, UK) explored the possibility that the gap between theory and practice in automated reasoning could be narrowed by a theory of practical automated reasoners as approximations algorithms. The present gap exists because properties that are the subject of theoretical research--properties such as soundness and completeness--do not interest developers of practical reasoning systems. Developers are concerned with whether their systems work well in practice, that they make an effective tradeoff between accuracy--the {\em degree} of soundness and completeness--and efficiency. A successful theory of automated reasoners as approximation algorithms would provide: metrics for quantifying, and methods for measuring, the accuracy and efficiency of reasoning systems over the distributions of problems they encounter; methodologies for identifying effective efficiency/accuracy tradeoffs; algorithms for obtaining the desired tradeoffs; and theorems identifying the limitations inherent in making these tradeoffs. After briefly reviewing existing research that has developed semantic characterizations of computationally-attractive approximations of entailment, the speakers noted that the question of how to quantify the accuracy of these approximation has been ignored. The talk then reviewed some of the key ideas and results from two areas where the notion of approximation has been used successfully: approximation algorithms for NP-complete optimization problems and the Probably Approximately Correct model of learning. Suggestions were made for how the key ideas from these areas might be adapted to the study of automated reasoning, and, in particular, to reasoning systems that adapt their approximations to the distributions of problems they encounter. As respondent, Tony Cohn (University of Leeds, UK) pointed out that reasoning with an abstraction of a theory can be viewed as approximate reasoning with the theory itself, and he referred to the work of Fausto Giunchiglia and Toby Walsh. Other participants suggested additional reasoning methods that could be viewed as making approximations. Panel: Reasoning about Large Specifications: How is it Possible? The panel was chaired by Jim Cunningham (Imperial College, UK), who introduced the topic by suggesting that the central issue was the extent and the means by which automated reasoning was applicable for those "big" things which we do not comprehend in full. It seems that with large specifications we have to cope with both component structure and with the details of individual components. While small individual components were amenable to automated reasoning, a logic of outline reasoning seems to be necessary for comprehending the whole specification. Stuart Anderson (University of Edinburgh, UK) addressed high integrity systems, an industrial motive for reasoning about specifications to eliminate faults. Stuart referred to the experience of the Voyager and Galileo Spacecraft, where almost all faults were specification errors, not programming mistakes. While the best way of avoiding problems with large specifications was to keep them small, the Edinburgh group were also examining industrial electronic controller languages to clarify their semantics and were investigating weakly expressive formal systems for ease of explication. Wolfgang Reif (University of Karlruhe, Germany), described the methodology of the Karlruhe Interactive Verifier (KIV), which presently is geared to verify sequential programs of up to 10,000 lines. The success of the system is attributed to its ability to combine the verification of small modules and to re-use earlier proofs in re-proving after a program or specification is modified. Most reasoning is done automatically, with occasional intervention for guidance. John Lee (University of Edinburgh, UK) completed the panel discussion by reporting efforts to provide a framework for graphics assisted reasoning, so that the interpretation of graphics elements is sound and complete, and visual abstraction can be exploited for interaction. Wrap-Up Session The discussion in the wrap-up session focused on what, if any, further activities could serve the members of the automated reasoning community, particularly those in the UK. There was a consensus that the workshop was productive, that further workshops would be desirable, that broad workshops were preferred to workshops focused on narrow topics, that the theme "Bridging the Gap between Theory and Practice" should be retained, and that the format of focused panel and talk sessions should be retained. There was broad support for the suggestion of including system demonstrations in the programme, and several people expressed interest in giving a system demonstration. Enthusiastic support was expressed for the suggestion of planning a one-day workshop along these lines for the 1995 AISB Conference in Sheffield. The workshop concluded with a well-attended and highly-productive session in a campus pub.