The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #774

Title:A Subsumption Architecture for Theorem Proving
Authors:Bundy,A
Date:Nov 1995
Presented:Published in Philosophical Transactions of the Royal Society of London, Series A, vol 349, pp 71-85 1994
Keywords:
Abstract:Brooks has criticised traditional approaches to Artificial Intelligence as too inefficient, [Brooks, 1991]. In particular, he has singled out techniques involving search as inadequate to achieve the fast reaction times required by robots and other AI products that need to work in the real world. Instead he proposes the subsumption architecture as an overall organising principle. This consists of layers of behavioural modules, each of which is capable of carrying out a complete (usually simple) task. He has employed this architecture to build a series of simple mobile robots, but he claims that it is appropriate for all AI products. Brooks' proposal is usually seen as an example of Nouvelle AI, in contrast to GOFAI (Good Old Fashioned AI - see Margaret Boden's contribution to this volume for more discussion of this contrast). Automatic theorem-proving is the archetypal example of GOFAI. The resolution theorem proving technique once served as the engine of AI. Of all areas of AI it seems most difficult to implement using Brooks' ideas. It would thus serve as a keen test of Brooks' proposal to explore to what extent the task of theorem-proving can be achieved by a subsumption architecture. Tactics are programs for guiding a theorem-prover, [Gordon et al, 1979]. They were introduced as an efficient alternative to search-based techniques. In this paper we will compare recent work on tactic-based theorem proving with Brooks' proposals and show that, surprisingly, there is a similarity between them. it thus seems that the distinction between Nouvelle AI and GOFAI is not so great as is sometimes claimed. However, this exercise also identifies some criticisms of Brooks' proposal.
Download:PDF COPY

[Search These Pages] [DAI Home Page] [Comment]