New uses of linear arithmetic in automated theorem proving by induction
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.
algorithm for generating induction schemes
decision procedure for Presburger arithmetic
scientific article; zbMATH DE number 887164
scientific article