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

Research Paper #934

Title:Automating the synthesis of decision procedures in a constructive metatheory
Authors:Armando,A; Gallagher,J; Smaill,AD; Bundy,A
Date:Nov 1998
Presented:Accepted for publication in Annals of Mathematics and Artificial Intelligence
Abstract:We present an approach to the automatic construction of decision procedures, via a detailed example in propositional logic. The approach adapts the methods of proof-planning and the heuristics for induction to a new domain, that of meta-theoretical procedures. This approach starts by providing an alternative characterisation of validity; the proofs of that correctness and completeness of this characterisation, and the existence of a decision procedure, are then amenable to automation in the way we describe. In this paper we identify a set of principled extensions to the heuristics for induction needed to tackle the proof obligations arising in the new problem domain and discuss their integration within the CLAM-Oyster system.

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