Semantic generalizations for proving and disproving conjectures by analogy

Taking an extension of resolution as a base calculus (though the sane principles are applicable to other calculi) for searching proofs (refutations) and counterexamples (models), we introduce a new method able to find refutations and also models by analogy with refutations and models in a knowledge base, The source objects for the analogy process are generalizations of the refutations (models). They are included in the knowledge ase, and then higher-order matching techniques for the choice of the relevant source objects as well as the building of a new proof or a model by analogy are used. Some comparisons with existing methods as well as two detailed running examples on generalization show evidence of the interest of our approach.