Sound Lemma Generation for Proving Inductive Validity of Equations

Takahito Aoto
In many automated methods for proving inductive theorems, finding a suitable generalization of a conjecture is a key for the success of proof attempts. On the other hand, an obtained generalized conjecture may not be a theorem, and in this case hopeless proof attempts for the incorrect conjecture are made, which is against the success and efficiency of theorem proving. Urso and Kounalis (2004) proposed a generalization method for proving inductive validity of equations, called...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.