Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Gupta, A. (1994): Inductive Boolean Function Manipulation: A Hardware Verifieation Methodology tor Automatic Induction. Ph.D. Thesis, CMU, Pittsburgh.
Boyer, R.S., and Moore, J.S. (1988): A Computational Logic Handbook. Academic Press.
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).
Bryant, R.E. (1986): “Graph-based algorithms for boolean function manipulation,” IEEE Trans. on Computers, C-35(8).
Dershowitz, N. (1986): “Termination of rewriting,” J. Symbolic Computation, 3, 69–116.
Enderton, H. (1972): A MathematiCal Introduction to Logic. Academic Press.
Kapur, D. (1994): “Automated tools for analyzing completeness of specifications,” Proc. 1994 Intl. Symp. on Software Testing and Analysis (ISSTA), Seattle, WA.28–43.
Kapur, D. (1997a): “Shostak’s congruence closure as completion,” Proc. Intl. Conf. on Rewriting Techniques and Applications (RTA-91), Barcelona, Spain.
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.
Kapur, D., Narendran, P., Rosenkrantz, D., and Zhang, H. (1991): “Sufficient-completeness, quasi-reducibility and their complexity,” Acta Informatica, 28,311–350.
Kapur, D., and Nie, X. (1994): “Reasoning about numbers in Tecton,” Proc. 8th Intl. Symp. Methodologies tor Intelligent Systems, Charlotte, North Carolina, 57–70.
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.
Kapur, D., and Subramaniam, M. (1996b): “Mechanically verifying a family of multiplier circuits,” Proc. CAV, (eds. Alur and Henzinger), LNCS 1102, 135–146.
Kapur, D., and Subramaniam, M. (1997): “Mechanizing reasoning about arithmetic circuits: SRT division,” Proc. 17th FSTTCS, Springer LNCS 1346, Kharagpur, India.
Kapur, D., and Subramaniam, M. (1998a): “Mechanical verification of adder circuits using powerlists,” J. Formal Methods in System Design, 13(2), 127–158.
Kapur, D., and Subramaniam, M. (1998b): “Mechanizing reasoning about large finite tables in a rewrite based theorem prover,”, Proc. ASIAN-98, LNCS 1538, Manila.
Kapur, D., and Subramaniam, M. (2000a): “Extending decision procedures with induction schemes” Proc. CADE-17 (ed. McAllester) Springer LNAI 1831, Pittsburgh.
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.
Kapur, D., and Zhang, H. (1995): “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 91–114.
Nelson, G., and Oppen, D.C. (1979): “Simplification by unnperating decision procedures,” ACM Trans. on Programming Languages and Systems 1 (2), 245–257.
Shostak, R.E. (1984): “Deciding combination of theories,” J. ACM 31 (1), 1–12.
Subramaniam, M. (1997): Failure Analyses in Inductive Theorem Provers. Ph.D. Thesis, Department of Computer Science, University of Albany, New York.
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.
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.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Wien
About this paper
Cite this paper
Kapur, D. (2001). Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic. In: Alefeld, G., Rohn, J., Rump, S., Yamamoto, T. (eds) Symbolic Algebraic Methods and Verification Methods. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6280-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6280-4_13
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-83593-7
Online ISBN: 978-3-7091-6280-4
eBook Packages: Springer Book Archive