Trivializing the proof of trivial theorems
Yves Kodratoff, Jacqueline Castaing · International Joint Conference on Artificial Intelligence · 1983
Besides a definition of theorem, this paper presents a sketch of our methodology for the generalization of recurrence proofs on trivial theorems but that lead, in a context of automatic theorem proving, to very lengthy (or even impossible to achieve) proofs. This paper reduces to a description of a detailed example, we hope to make clear that our methodology is of a much wider field of application.