New uses of linear arithmetic in automated theorem proving by induction

DOI10.1007/BF00244459zbMath0851.03002OpenAlexW2006104711MaRDI QIDQ1915133

Deepak Kapur, Mahadevan Subramaniam

Publication date: 4 November 1996

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244459

zbMATH Keywords

semantic unificationalgorithm for generating induction schemesdecision procedure for Presburger arithmeticgeneralization of cover set methodproof by explicit inductiontheorem prover RRL

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Automated reasoning about parallel algorithms using powerlists ⋮ Lemma discovery in automating induction

Uses Software

• NQTHM
• RRL
• Tecton

Cites Work

• Termination of rewriting
• An overview of the Tecton proof system
• Automatic proofs by induction in theories without constructors
• Sufficient-completeness, ground-reducibility and their complexity
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: New uses of linear arithmetic in automated theorem proving by induction