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 |
| Keywords: | |
| 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. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}