New uses of linear arithmetic in automated theorem proving by induction (Q1915133)

The `cover set method' is an algorithm for generating induction schemes for proof by explicit induction. It uses syntactic unification to generate schemes in a setting where functions are defined by finite sets of terminating rewrite rules. The authors provide a generalization based on semantic unification where a decision procedure for Presburger arithmetic is used to provide the semantic analysis. The unique prime factorization theorem of number theory is used as a nontrivial example to demonstrate how this generalization helps automate inductive theorem proving in the context of the theorem prover RRL.