Original language | English |
---|
Journal | Annals of Mathematics and Artificial Intelligence |
---|
Volume | 22 |
---|
Issue number | 3-4 |
---|
Publication status | Published - 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.
ID: 402400