Working Notes

1995 AISB Workshop Series

Automated Reasoning: Bridging the Gap between Theory and

Practice

University of Sheffield April 4^{th}, 1995

Programme Chair: Andrew Ireland

Foreword

This is the second Automated Reasoning workshop held in association with AISB on the theme of “Bridging the Gap between Theory and Practice”. The broad spectrum of interests reflected in this collection of abstracts demonstrates the important role such a workshop series plays in fostering links and facilitating cross-fertilization of ideas among researchers from various disciplines.

As Programme Chair I am indebted to my fellow members of the Organizing Committee for their support and guidance: Alan Bundy (Edinburgh), Barry Crabtree (BT Labs, Ipswich), Alan Frisch (Chair, York), Roger Jones (ICL, Wokingham), Antony Galton (Exeter). Thanks also go to Craig MacNish (York) who assisted with publicity.

We would like to thank AISB for sponsoring this workshop and for their organisational help, in particular Robert Gaizauskas. Finally we acknowledge the financial support of the Compulog Net.

Andrew Ireland Programme Chair

Contents

Jonas Barklund & Patricia M. Hill

Logic Programming with Restricted Quantifications and Arrays . . . . . . . . . . . . . . . . 1 Peter Baumgartner, Ulrich Furbach & Frieder Stolzenburg

Computing Answers and Logic Programming by Model Elimination Based Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

Brandon Bennett

Towards a Decision Procedure for the RCC Theory of Spatial Regions . . . . . . . . . 5 Narjes Berregeb & Michael Rusinowitch

Extending induction proofs in associative and commutative theories . . . . . . . . . . . . 8 Marc Bezem & Jan Friso Groote

Proving a Graph Well Founded using Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Wolfgang Bibel & Michael Thielscher

The Role of Automated Deduction in Intellectics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 James E. Borrett

Observations on the Usefulness of AC Preprocessing . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Paolo Bresciani, Enrico Franconi & Sergio Tessaris

Implementing and testing expressive Description Logics . . . . . . . . . . . . . . . . . . . . . . 17 Alan Bundy

Relational Rippling: A General Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Maria R. Cravo

A Computational System for Commonsense Reasoning . . . . . . . . . . . . . . . . . . . . . . . 20 Paul Curzon, Ian Leslie & Mike Gordon

Conclusions from a Study to Verify a Real Network Component . . . . . . . . . . . . . . 22 Andrew Davenport

A Closer Look at the Exceptionally Hard Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 David Duffy, Craig MacNish & Miles Osborne

Practical Issues in Applying Automated Reasoning to Requirements Analysis . 26 Floriana Esposito, Nicola Fanizzi, Donato Malerba & Giovanni Semeraro

Inductive Reasoning for Document Classification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Saturnino F. Luz Filho

Reasoning about intentions: theoretical and practical issues . . . . . . . . . . . . . . . . . . 31 Michael Fisher

Flexible Concurrent Theorem-Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Alan M. Frisch & Edmund J. A. Dumbill

Solving Constraint Satisfaction Problems with MV-Resolution: Initial Investigations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

R. Garigliano, Z. Luo, D.J. Nettleton, S. Poria, N. Shah, S. Shiu, S. Short Knowledge Representation and Reasoning Using Sorts in Large Scale Natural Language Processing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

Ian P. Gent & Toby Walsh Phase Transitions: Helping to Bridge the Gap between Theory and Practice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

Alan G. Hamilton

Interactive Theorem-Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Dieter Hutter & Werner Stephan

Deduction in Verification Support Environments (VSE) . . . . . . . . . . . . . . . . . . . . . . 43 Andrew Ireland

Towards a Logical Basis for Heuristic Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . 45 Robert Johnson

Developing Automated Temporal Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Zhaohui Luo

Developing Reuse Technology in Proof Engineering . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Simin Nadjm-Tehrani

Verification of a Landing Gear: a Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Maurice Naftalin

Investigating the Industrial Applicability of Proof Planning . . . . . . . . . . . . . . . . . . . 55 Cyrus F. Nourani & Thomas Hoppe

G-Diagrams for Models, Free Proof Trees and Abductive Automated Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

Cyrus F. Nourani

Free Proof Trees and Model-Theoretic Planning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 Miguel-Angel Oros & Paul Y. Gloess

Inferring Inheritance Hierarchies from Datalog Programs . . . . . . . . . . . . . . . . . . . . . 61 Patrick Prosser

Phase Transitions: A brief history of the phenomenon in binary constraint satisfaction problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

Barbara M. Smith & Stuart A. Grant

Phase Transition Behaviour and Algorithm Performance . . . . . . . . . . . . . . . . . . . . . . 66 H.C.M. de Swart & E.A. de Kogel

Algebraic Characterizations of Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 Mark Tarver

Reconstructing the Boyer-Moore Theorem Prover Within a Theory of Modules for Functional Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 An Algorithm for Inducing Tactics from Sequentzen Proofs . . . . . . . . . . . . . . . . . . . 72

Judith Underwood

Extended ML: A challenge to automated reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 Laurent Vigneron

Efficient Strategies for Automated Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

Abstracts

v