Now showing items 1-3 of 3
Increasing the Versatility of Heuristic Based Theorem Provers
(Springer Verlag, 1993)
Heuristic based theorem proving systems typically impose a fixed ordering on the strategies which they embody. The ordering reflects the general experience of the system designer. As a consequence, there will exist a variety ...
Rippling: A Heuristic for Guiding Inductive Proofs
We describe rippling: a tactic for the heuristic control of the key part of proofs by mathematical induction. This tactic significantly reduces the search for a proof of a wide variety of inductive theorems. We first present ...
Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs
(Springer Verlag, 1990)
In earlier papers we described a technique for automatically constructing inductive proofs, using a heuristic search control tactic called rippling-out. Further testing on harder examples has shown that the rippling-out ...