We present an approach to tackle theorem-proving problems by difference reduction techniques. The rippling calculus developed in the field of inductive theorem proving is used to maintain differences throughout the deduction. Syntactical abstractions of the differences are used to sketch abstract proofs which are refined with the help of rippling techniques. This technique results in a highly goal-oriented and hierarchical approach which is also well-suited for interactive theorem proving.
Automated Deduction, Proof Planning, Difference Reduction, Abstractions, Rippling