Mechanising Deduction in the Logics of Practical Reasoning

Description

Project Title:
Mechanising Deduction in the Logics of Practical Reasoning
Acronym:
MEDLAR II
Number:
6471
Work Area:
Knowledge Engineering & Representation
Coordinator:
The Imperial College of Science, Technology & Medicine
180 Queen's Gate
UK - LONDON SW7 2BZ
Coordinator Country:
UK
Partners
RISC A
Max Planck Institüt für Informatik D
Technische Hochschule Darmstadt D
Technische Universität München D
INPG F
ONERA-CERT F
Université Paul Sabatier Toulouse F
Università di Torino I
University of Oslo N
ICL UK
Contact Point:
Mr. J. Cunningham
Telephone:
+44/71-5895111 Ext. 5045
Fax:
+44/71-5818024
E-Mail:
rjc@doc.ic.ac.uk
Keywords:
mechanised logic, labelled deduction, abduction, theorem proving, automated reasoning, non-classical logic, temporal logic, modal logic, practical reasoning, natural language dialogue, robotics, geometric reasoning
Start Date:
24 July 1992
Duration:
36 months
Status:
running
Abstract:
MEDLAR II builds on the success of the original MEDLAR project (3125) in developing a general framework for mechanising deduction in the logics of practical reasoning - the philosphical term for logics of time, action, belief, knowledge and duty. In Medlar II the concept of a practical reasoner will be developed, an agent capable of acting autononously and interacting flexibly with its real-world environment.

AIMS

The programme of MEDLAR II aims to refine and develop the MEDLAR technologies, seeking:
- the synthesis of specific capabilities like abduction, analogy, planning and model building in a given combination of logics
- the development of the general framwework to produce specific reasoning capabilities
- exploration of the architecture for specialisation, implementation and integration in a generic practical reasoning agent.
Scientifically we seek to advance and disseminate a framework for knowledge representation and reasoning which is cognisant of the principles and practice of mechanised deduction in the logics of practical reasoning.
In practical terms we must reconcile the vision of a generic conceptual system, the "MEDLAR Practical Reasoner" with more concrete individual perspectives, so that we can develop small demonstrators for case studies in natural language dialogue and in robotic reasoning.
In MEDLAR II the concept of a practical reasoner will be developed, an agent capable of acting autonomously and interacting flexibly with its real-world environment. A human practical reasoner is distinguished from an artificial machine in many aspects, but for the purpose of the project we are chiefly concerned with two. The first is the rich variety of common sense reasoning methods - temporal, modal, probabilistic, relevant, abductive, hypothetical etc. The second aspect is an ability to interface and join together different modes of reasoning into one complex system: a practical reasoning agent.

APPROACH AND METHODS

The project will be motivated by case studies in natural language dialogue, the safety and security of databases and in robotics. It will address certain key steps in knowledge representation and reasoning with the logics of practical reasoning, namely the synthesis of specific reasoning capabilities like abduction, analogy, planning and model building. We seek to place these capabilities within an integrating framework which can be shown to have a basis for implementation.
Five tasks, co-ordinated by management meetings and scientific workshops are intended to deliver both scientific progress for the wider community and demonstrations of feasible application.

PROGRESS AND RESULTS

The interim results of the first subtasks in the case studies, specific reasoning capabilities, the general framework and its mechanisation were presented at a review workshop in Leeds.
The outline of a general deductive framework for mixing various logics and calculi has emerged from MEDLAR I and is being developed to deal with specific reasoning capabilities. For an early paper on the overall perspective see Cunningham, Gabbay & Ohlbach (1991), for a specific contribution to abductive reasoning see Nossum and Gabbay (1993).

POTENTIAL

Future work in the MEDLAR II project includes the design of a MEDLAR Practical Reasoner, a concept which can be specialised in many ways but which will in practice be specialised to the needs of specific case studies in the project. Nevertheless, progress suggests that new technologies for abductive logic programming, efficient model building on parallel machines, and other novel approaches in the areas of the case studies will have potential for exploitation in more applied industrial projects.

LATEST PUBLICATIONS

INFORMATION DISSEMINATION ACTIVITIES

The following workshops were arranged to focus the scientific activities of the project. Most involved a small number of external scientific collaborators and invited representatives of other European projects.
- Start-up workshop, Lillesand, Norway, September 1992
- 6 month workshop, Garmisch, Germany, January 1993
- 12 month workshop and review, Leeds UK, July 1993
The deliverables of the first review workshop are available by anonymous file transfer from Imperial College.
Arrangements for the 18 month and 24 month workshops can be found from the contact given above. It is intended to promote an open workshop at international conference in 1994.
A demonstration of the Technical University of Munich SETHEO theorem prover was given at IJCAI-93. This was developed partly with support from the MEDLAR projects.

Sven Müßig, last update 07-nov-1995. Your feedback is welcome.