Specifying an Automated Induction Proof Procedure in ASF+SDF
D. Naidich & T.B. Dinesh (Iowa, CWI)
(Available as P9504-13.ps.gz)
Abstract
We describe the implementation of an automated theorem prover for
algebraic specifications, in an algebraic specification setting using
the ASF+SDF Meta-environment. The current implementation is based on
the implicit induction approach implemented in SPIKE
[Spike,Spike1]. We consider the implementation as a case study on the
tool generation within ASF+SDF which also provides an experimental
basis for the research on automated induction. We consider the issues
of the simplification strategies of implicit induction, the user
interaction/heuristics in implicit induction, the computational
effectiveness of ASF+SDF specifications, and the plausible
improvements of the ASF+SDF specification language.