Implementing Reasoning Modules in Implicit Induction Theorem Provers
Sorin Ioan Stratulat · 2014
We detail the integration in SPIKE, an implicit induction theorem prover, of two reasoning modules operating over naturals combined with interpreted symbols. The first integration schema is à la Boyer-Moore, based on the combination of a congruence closure procedure with a decision procedure for linear arithmetic over rationals/reals. The second follows a 'black-box' approach and is based on external SMT solvers. It is shown that the two extensions significantly increase the power of SPIKE, their performances are compared when proving a non-trivial application.