Edinburgh Research Explorer

Automating the Synthesis of Decision Procedures in a Constructive Metatheory

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions

Open

Documents

Original languageEnglish
JournalAnnals of Mathematics and Artificial Intelligence
Volume22
Issue number3-4
StatePublished - 1998

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 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