6 - From rippling to a general methodology

Summary

This book has described rippling: a technique for guiding proof search so that a given may be used to prove a goal. We will investigate in this chapter other areas of automated reasoning involving heuristic restrictions on proof search. We will use problems from these areas to illustrate how the ideas behind rippling can be generalized and used systematically to understand and implement many different kinds of deductive reasoning.

• many proof calculi, the application of rules in certain situations is known to be unnecessary and can be pruned without sacrificing completeness. For example, in basic ordered paramodulation and basic superposition (Bachmair et al., 1992; Nieuwenhuis & Rubio, 1992), paramodulation is forbidden into terms introduced by applying substitutions in previous inference steps.

• tactic-based theorem-proving, it is sometimes useful to track parts of the conjecture and use this to restrict proof search. Focus mechanisms (e.g. Robinson & Staples, 1993; Staples, 1995) for this purpose have been developed and hardwired into several calculi.

• analogical reasoning, a previous proof (the source proof) is abstracted to serve as a proof template for subsequent conjectures (the target conjecture). Additional information about the source proof (in addition to the proof tree) is typically required to compute an abstract proof sketch (Kolbe & Walther, 1994; 1998) for a related target conjecture

In each of the above techniques, there is a need to encode and maintain information about individual terms and symbols and their inter-relationships.