Mechanizing Inductive Reasoning

9 years 10 months ago
Mechanizing Inductive Reasoning
Automating proofs by induction is important in many computer science and artificial intelligence applications, in particular in program verification and specification systems. We present a new method to prove (and disprove) automatically inductive properties. Given a set of axioms, a well-suited induction scheme is constructed automatically. We call such a scheme a test-set. Then, for proving a property, we just instantiate it with terms from the test-set and apply pure algebraic simplification to the result. This method avoids completion and explicit induction. However it retains their positive features, namely the completeness of the former and t,he robustness of the latter.
Emmanuel Kounalis, Michaël Rusinowitch
Added 06 Nov 2010
Updated 06 Nov 2010
Type Conference
Year 1990
Where AAAI
Authors Emmanuel Kounalis, Michaël Rusinowitch
Comments (0)