Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic
- 1 January 2001
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem ProverPublished by Springer Nature ,1998
- Mechanical Verification of Adder Circuits using Rewrite Rule LaboratoryFormal Methods in System Design, 1998
- Shostak's congruence closure as completionPublished by Springer Nature ,1997
- Rewriting, decision procedures and lemma speculation for automated hardware verificationPublished by Springer Nature ,1997
- New uses of linear arithmetic in automated theorem proving by inductionJournal of Automated Reasoning, 1996
- Mechanically verifying a family of multiplier circuitsPublished by Springer Nature ,1996
- An overview of Rewrite Rule Laboratory (RRL)Computers & Mathematics with Applications, 1995
- Sufficient-completeness, ground-reducibility and their complexityActa Informatica, 1991
- Termination of rewritingJournal of Symbolic Computation, 1987
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986