The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #836

Title:An Experimental Comparison of Rippling and Exhaustive Rewriting
Authors:Bundy,A; Green,I
Date:Dec 1996
Presented:Submitted to the Conference on Automated Deduction, 1997
Abstract:We compare rippling and exhaustive rewriting using recursive path orderingk on a range of inductive proofs. We present statistics on success rates, branching rates and CPU times. We use these statistics to argue that rippling succeeds more often. However, these statistics also show that rippling and reduction are roughtly roughly the same in terms of average branching rate and that rippling often takes longer in terms of CPU time.

[Search These Pages] [DAI Home Page] [Comment]