==== FIRST WORKSHOP ON AUTOMATED REASONONG ====
===== TIMETABLE =====
== MONDAY, April 11 ==
11.00 - 11.30 Welcome and Coffee
11.30 - 1.00 The Role of Interaction in Automated Deduction
Introduction (10 mins)
Panel Presentations (40 mins)
Open Discussion (40 mins)
1.00 - 2.00 Lunch
2.00 - 3.30 Logic Program Specialization and Approximation
for Optimizing Theorem Provers
Speakers (40 mins)
Response (10 mins)
Open Discussion (40 mins)
3.30 - 4.00 Tea
4.00 - 5.30 Automating Temporal Non-Monotonic Reasoning
Introduction (10 mins)
Panel Presentations (40 mins)
Open Discussion (40 mins)
== TUESDAY, April 12 ==
9.00 - 11.00 Comparing and Evaluating Proof Calculi
Introduction (10 mins)
Panel Presentations (50 mins)
Open Discussion (60 mins)
11.00 - 11.30 Coffee
11.30 - 12.45 Wanted: A Theory of Approximation for Automated Reasoning
Speakers (30 mins)
Response (10 mins)
Open Discussion (35 mins)
12.45 - 1.30 Lunch
1.30 - 2.00 AISB AGM
2.00 - 3.30 Reasoning about Large Specifications: How is it Possible?
Introduction (10 mins)
Panel Presentations (35 mins)
Open Discussion (45 mins)
3.30 - 4.00 Tea
4.00 - 4.30 Wrap-up session
===== PROGRAM =====
Talk: Logic Program Specialization and Approximation for Optimizing
Theorem Provers
Speakers: John Gallagher and Andre de Waal
Respondent: Pat Hill
Moderator: John Derrick
Abstract: Program specialization (or partial evaluation) has often
been applied to to the optimization of meta-programs, especially
language interpreters. In this talk we see how specialization
techniques can be applied effectively to proof procedures. A proof
procedure is specialized with respect to a given object theory (and
possibly a theorem as well). This can sometimes result in
substantial reductions in proof search, as will be seen from
experiments. The method is applicable to any proof procedure that
can be expressed as a logic program.
--------------
Panel: The Role of Interaction in Automated Deduction
Moderator: Andrew Ireland
Panelists: John Derrick, David Duffy, Anton Setzer, Mark Tarver
Abstract: Automated deduction systems that operate on highly
expressive languages or that construct inductive proofs usually
require some kind of human assistance. What is the proper role of
human interaction in automated reasoning? Should we attempt to
minimize or eliminate the use of human assistance in automated
reasoning? If so, how can this be achieved? If human assistance is
not eliminated, how can logical languages and deductive systems be
designed to facilitate interaction?
--------------
Panel: Automating Temporal Non-Monotonic Reasoning
Moderator: Antony Galton
Panelists: John Bell, John Gooday, Robert Kowalski, Craig MacNish
Abstract: Non-monotonic temporal reasoning is a necessary part of
commonsense reasoning and has numerous applications in areas such as
planning, diagnosis and natural language understanding. A decade of
theoretical work has led to the development of several promising
formalisms for non-monontonic temporal reasoning, each capable of
solving a wide variety of significant problems on paper. However,
very little work has been done on developing automated methods for
reasoning with these formalisms. This panel and subsequent
discussion will address the question: To what extent can
non-monotonic reasoning in general, and temporal non-monotonic
reasoning in particular, be handled by adapting the methods and
techniques that have proved successful in automating monotonic
reasoning? Or does the automation of non-monotonic reasoning
require a radically different approach?
--------------
Panel: Comparing and Evaluating Proof Calculi
Moderator: Reiner Haehnle
Panelists: Bernhard Beckert, Eric de Kogel, Harrie de Swart,
Ulrich Furbach, Robert Johnson
Abstract: Many calculi have been used as the basis of automated
deduction for first-order logic: resolution, the connection method,
tableau, model elimination, and methods based on term-rewriting.
What criteria should be used in evaluating these calculi, and how do
the various calculi compare under these criteria? Criteria of
potential interest include: o How easy is it to integrate
specialized reasoners into the calculus? o How effectively can
deduction with the calculus be controlled? o How much redundancy
does the calculus introduce into the search space and what methods
exist for reducing the redundancy? o Can the calculus be used for
constructing proofs, refutations, and models? o Can the calculus be
automated efficiently? Is it amenable to parallel implementations?
o How amenable is the calculus to proof by induction? o How natural
are proofs expressed in the calculus?
--------------
Talk: Wanted: A Theory of Approximation for Automated Reasoning
Speakers: C. David Page and Alan M. Frisch
Respondent: Tony Cohn
Moderator: Pat Hill
Abstract: Properties that are the subject of theoretical research on
automated reasoning--properties such as soundness, completeness and
optimality--do not interest developers of practical reasoning
systems; system developers are concerned with whether their systems
work well in practice. Consequently the field of automated
reasoning lacks relevant theories that allow general, fair,
constructive analyses and comparisons of practical systems. This
gap between theory and practice is not unique to automated
reasoning; recognition of a similar gap in optimisation has led to a
number of useful theoretical results about the quality of
approximation algorithms. This talk explores the possibility that,
by viewing practical reasoning systems as approximation algorithms,
similar methods may be used to help bridge the gap between theory
and practice in automated reasoning. A framework for exploring
issues in approximation for automated reasoning is presented, and
the state of the art is surveyed.
--------------
Panel: Reasoning about Large Specifications: Is it Possible?
Moderator: Jim Cunningham
Panelists: Stuart Anderson, John Lee, Wolfgang Reif
Abstract: What distinct goals are there for reasoning about
industrial scale specifications? Is automated design and
verification of large software systems tractible, or should we
perhaps seek merely to assist in human comprehension? (Perhaps we
should be talking about formal systems in general and not just
specifications). When can crucial features, perhaps for safety, be
proved in isolation? Will a friendly human interface for dealing
with large specifications necessarily lose rigour? Some devices that
have been proposed for dealing with these issues are:
o Structural simplification through objects or fibering,
o Environments which separate proof tactics from proof calculi,
o Natural deduction and natural language proof presentations,
o Executable specifications for informal validation,
o Graphics-assisted reasoning.
We need views on the way forward which will reflect industrial needs as
well as formal insight if we are to make technology from the automated
reasoning community widely applicable for industrial scale problems.