Automating Inductive Specification Proofs
Brigitte Pientka, Christoph Kreitz · Fundamenta Informaticae · 1999
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. Und