Analogy and Abduction in Automated Deduction

摘要

A method is presented for analgoical reasoning in Automated Deduction. We focus on the abductive aspects of analogy and give a unified treatment for theorems and non-theorems. Abduction allows to deal with partial analogies thus strongly increasing the application field of the mehtod. It also allows to detect "bad analogies" in several cases. Explanatory examples as well as more realistic examples quantifying the effects of using analogy (for theorem-proving and for counter-example building )are given.