Affiliations: Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA | Department of Computer Science, Cornell University, Ithaca, NY, USA
Note: [] Address for correspondence: Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
Note: [] Address for correspondence: Department of Computer Science, Cornell University, Ithaca, NY, USA
Abstract: We present an automatic method which combines logical proof search and rippling heuristics to prove specifications. The key idea is to instantiate meta-variables in the proof with a simultaneous match based on rippling/reverse rippling heuristic. Underlying our rippling strategy is the rippling distance strategy which introduces a new powerful approach to rippling, as it avoids termination problems of other rippling strategies. Moreover, we are able to synthesize conditional substitutions for meta-variables in the proof. The strength of our approach is illustrated by discussing the specification of the integer square root and automatically synthesizing the corresponding algorithm. The described procedure has been integrated as a tactic into the NUPRL system but it can be combined with other proof methods as well.
Keywords: theorem proving, program synthesis, induction
