Rewriting Induction + Linear Arithmetic = Decision Procedure

Abstract. 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.

• Type: Journal
• Year: 2012
• Where: CADE
• Authors: Stephan Falke, Deepak Kapur
• Keywords: CADE 2012, Integer Arithmetic, Logical Reasoning, Prototype Implementation, Rewrite Systems