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