New uses of linear arithmetic in automated theorem proving by induction
type: Item
instance of: scholarly article
title: New uses of linear arithmetic in automated theorem proving by induction
zbMATH Open document ID: 0851.03002
DOI: 10.1007/BF00244459
author: Deepak Kapur
author: Mahadevan Subramaniam
published in: Journal of Automated Reasoning
publication date: 1996-11-04T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 887164
zbMATH Keywords: generalization of cover set method
zbMATH Keywords: algorithm for generating induction schemes
zbMATH Keywords: proof by explicit induction
zbMATH Keywords: semantic unification
zbMATH Keywords: decision procedure for Presburger arithmetic
zbMATH Keywords: theorem prover RRL
reviewed by: David Basin
describes a project that uses: NQTHM
describes a project that uses: RRL
describes a project that uses: Tecton
MaRDI profile type: Publication
cites work: Q3894958
cites work: Q4040283
cites work: Q3835049
cites work: Termination of rewriting
cites work: Automatic proofs by induction in theories without constructors
cites work: An overview of the Tecton proof system
cites work: Sufficient-completeness, ground-reducibility and their complexity
cites work: Q3805961
full work available at URL: https://doi.org/10.1007/bf00244459
OpenAlex ID: W2006104711
Recommended article: An even closer integration of linear arithmetic into inductive theorem proving
Recommended article: Proof synthesis and reflection for linear arithmetic
Recommended article: Q4217606
Recommended article: Using an induction prover for verifying arithmetic circuits
Recommended article: The automation of proof by mathematical induction
Recommended article: Proofs as computations in linear logic
Recommended article: Recent advances in automated theorem proving on inequalities
Recommended article: Q4548193
Recommended article: On automating diagrammatic proofs of arithmetic arguments
description: scientific article; zbMATH DE number 887164