Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic

  • Deepak Kapur


Theorem provers and automated reasoning tools are not as widely used in specification analysis, debugging and verification of hardware and software as one would hope. A major reason is perhaps that these tools are often found difficult to use. The learning curve for a typical theorem prover is quite high; it takes a great deal of effort by typical users to effectively use such a tool for their application domain. Even then, considerable resources must be expended by building a large knowledge base and library of useful properties in a representation suitable for the prover, to bring it to a level so that it can start playing a useful role.


Decision Procedure Function Symbol Function Definition Recursive Call Induction Scheme 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Gupta, A. (1994): Inductive Boolean Function Manipulation: A Hardware Verifieation Methodology tor Automatic Induction. Ph.D. Thesis, CMU, Pittsburgh.Google Scholar
  2. Boyer, R.S., and Moore, J.S. (1988): A Computational Logic Handbook. Academic Press.Google Scholar
  3. Boyer, R.S., and Moore, J.S. (1988): “Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic”, Machine Intelligence 11, P. Hayes, D. Mitchie and J. Richards (eds).Google Scholar
  4. Bryant, R.E. (1986): “Graph-based algorithms for boolean function manipulation,” IEEE Trans. on Computers, C-35(8).Google Scholar
  5. Dershowitz, N. (1986): “Termination of rewriting,” J. Symbolic Computation, 3, 69–116.MathSciNetCrossRefGoogle Scholar
  6. Enderton, H. (1972): A MathematiCal Introduction to Logic. Academic Press.Google Scholar
  7. Kapur, D. (1994): “Automated tools for analyzing completeness of specifications,” Proc. 1994 Intl. Symp. on Software Testing and Analysis (ISSTA), Seattle, WA.28–43.Google Scholar
  8. Kapur, D. (1997a): “Shostak’s congruence closure as completion,” Proc. Intl. Conf. on Rewriting Techniques and Applications (RTA-91), Barcelona, Spain.Google Scholar
  9. Kapur, D. (1997b): “Rewriting, decision procedures and lemma speculation for automated hardware verification,” Proc. Theorem Provers in Higher-order Logics, (ed. Gunter and Felty), Springer LNCS 1275, Murray Hill, 171–182.Google Scholar
  10. Kapur, D., Narendran, P., Rosenkrantz, D., and Zhang, H. (1991): “Sufficient-completeness, quasi-reducibility and their complexity,” Acta Informatica, 28,311–350.MathSciNetMATHCrossRefGoogle Scholar
  11. Kapur, D., and Nie, X. (1994): “Reasoning about numbers in Tecton,” Proc. 8th Intl. Symp. Methodologies tor Intelligent Systems, Charlotte, North Carolina, 57–70.Google Scholar
  12. Kapur, D., and Subramaniam, M. (1996a): “New uses of linear arithmetic in automated theorem proving for induction,” J. Automated Reasoning, 16(1–2), 39–78.MathSciNetMATHCrossRefGoogle Scholar
  13. Kapur, D., and Subramaniam, M. (1996b): “Mechanically verifying a family of multiplier circuits,” Proc. CAV, (eds. Alur and Henzinger), LNCS 1102, 135–146.Google Scholar
  14. Kapur, D., and Subramaniam, M. (1997): “Mechanizing reasoning about arithmetic circuits: SRT division,” Proc. 17th FSTTCS, Springer LNCS 1346, Kharagpur, India.Google Scholar
  15. Kapur, D., and Subramaniam, M. (1998a): “Mechanical verification of adder circuits using powerlists,” J. Formal Methods in System Design, 13(2), 127–158.CrossRefGoogle Scholar
  16. Kapur, D., and Subramaniam, M. (1998b): “Mechanizing reasoning about large finite tables in a rewrite based theorem prover,”, Proc. ASIAN-98, LNCS 1538, Manila.Google Scholar
  17. Kapur, D., and Subramaniam, M. (2000a): “Extending decision procedures with induction schemes” Proc. CADE-17 (ed. McAllester) Springer LNAI 1831, Pittsburgh.Google Scholar
  18. Kapur, D., and Subramaniam, M. (2000b): D. Kapur and M. Subramaniam, “Using an induction prover for verifying arithmetic circuits,” J. Software Tools for Technology Transfer, Springer Verlag, Sep 2000.Google Scholar
  19. Kapur, D., and Zhang, H. (1995): “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 91–114.MathSciNetCrossRefGoogle Scholar
  20. Nelson, G., and Oppen, D.C. (1979): “Simplification by unnperating decision procedures,” ACM Trans. on Programming Languages and Systems 1 (2), 245–257.MATHCrossRefGoogle Scholar
  21. Shostak, R.E. (1984): “Deciding combination of theories,” J. ACM 31 (1), 1–12.MathSciNetMATHCrossRefGoogle Scholar
  22. Subramaniam, M. (1997): Failure Analyses in Inductive Theorem Provers. Ph.D. Thesis, Department of Computer Science, University of Albany, New York.Google Scholar
  23. Zhang, H. (1992): “Implementing contextual rewriting,” Proc. 3rd Intl. Workshop on Conditional Term Rewriting Systems, (eds. Remy and Rusinowitch), Springer LNCS 656, France, 363–377.Google Scholar
  24. Zhang, H., Kapur, D., and Krishnamoorthy, M.S. (1988): “A mechanizable induction principle for equational specifications,” Proc. 9th Intl. Conf. Automated Deduction (CADE), (eds. Lusk and Overbeek), Springer LNCS 310, Chicago, 250–265.Google Scholar

Copyright information

© Springer-Verlag Wien 2001

Authors and Affiliations

  • Deepak Kapur

There are no affiliations available

Personalised recommendations