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.