Stephan Falke and Deepak Kapur:
Rewriting Induction + Linear Arithmetic = Decision Procedure
In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12), Manchester, UK.
Lecture Notes in Artificial Intelligence 7364, pages 241-255, 2012. ©Springer-Verlag
This paper presents new results on the decidability of inductive
validity of conjectures. For these results, a class of term rewrite
systems (TRSs) with built-in linear integer arithmetic is introduced
and it is shown how these TRSs can be used in the context of inductive
theorem proving. The proof method developed for inductive theorem
proving couples (implicit) inductive reasoning with a decision
procedure for the theory of linear integer arithmetic with (free)
constructors. The effectiveness of the new decidability results on a
large class of conjectures is demonstrated by an evaluation of the
prototype implementation Sail2.
Paper on SpringerLink