Edinburgh Research Explorer

Automating the Synthesis of Decision Procedures in a Constructive Metatheory

Research output: Contribution to journalArticlepeer-review

Related Edinburgh Organisations

Open Access permissions



Original languageEnglish
JournalAnnals of Mathematics and Artificial Intelligence
Issue number3-4
Publication statusPublished - 1998


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 metatheoretic procedures. This approach starts by providing an alternative characterisation of validity; the proofs of the 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 statistics

No data available

ID: 402400