Sail2 Sail2 is an automatic inductive theorem prover for term rewrite systems with built-in linear integer arithmetic. Author Stephan Falke Papers Stephan Falke, Deepak Kapur: Rewriting Induction + Linear Arithmetic = Decision Procedure. IJCAR 2012: 241-255