Abstract
The ability of a theorem prover to generate explicit derivations for the theorems it proves has major benefits for the testing and maintenance of the prover. It also eliminates the need to trust the correctness of the prover at the expense of trusting a much simpler proof checker. However, it is not always obvious how to generate explicit proofs in a theorem prover that uses decision procedures whose operation does not directly model the axiomatization of the underlying theories. In this paper we describe the modifications that are necessary to support proof generation in a congruence-closure decision procedure for equality and in a Simplex-based decision procedure for linear arithmetic. Both of these decision procedures have been integrated using a modified Nelson-Oppen cooperation mechanism in the Touchstone theorem prover, which we use to produce proof-carrying code. Our experience with designing and implementing Touchstone is that proof generation has a relatively low cost in terms of design complexity and proving time and we conclude that the software-engineering benefits of proof generation clearly outweighs these costs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ackermann, W.: Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)
Aspvall, B., Shiloach, Y.: A polynomial time algorithm for solving systems of linear inequalities with two variables per inequality. SIAM Journal on Computing 9(4), 827–845 (1980)
Bledsoe, W.W.: The Sup-Inf method in Presurger arithmetic. Technical report. University of Texas Math Dept. (December 1974)
Boyer, R., Moore, J.S.: A Computational Logic. Academic Press, London (1979)
Boulton, R.J.: A lazy approach to fully-expansive theorem proving. In: International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, pp. 19–38. North- Holland, Amsterdam (1992) IFIP Transactions
Boulton, R.J.: Efficiency in a Fully-Expansive Theorem Prover. PhD thesis. University of Cambridge (December 1993)
Boulton, R.J.: Combining decision procedures in the HOL system. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 75–89. Springer, Heidelberg (1995)
Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto (December 1998)
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. Journal of the ACM 27(4), 758–771 (1980)
Gordon, M.: HOL: A machine oriented formulation of higher-order logic. Technical Report 85. University of Cambridge, Computer Laboratory (July 1985)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1(4), 497–536 (1991)
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157 (1991)
Necula, G.C.: Proof-carrying code. In: The 24th Annual ACM Symposium on Principles of Programming Languages, pp. 106–119. ACM, New York (1997)
Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (September 1998), Also available as CMU-CS-98-154
Nelson, G.: Techniques for program verification. Technical Report CSL- 81-10, Xerox Palo Alto Research Center (1981)
Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Paulson, L.C.: Isabelle: A generic theorem prover. LNCS, vol. 828, p. 321. Springer, Heidelberg (1994)
Pfenning, F.: Logic programming in the LF logical framework. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 149–181. Cambridge University Press, Cambridge (1991)
Pfenning, F.: Elf: A meta-language for deductive systems (system description). In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 811–815. Springer, Heidelberg (1994)
Pratt, V.R.: Two easy theories whose combination is hard(1977) (unpublished manuscript)
Stump, A., Dill, D.L.: Generating proofs from a decision procedure. In: Pnueli, A., Traverso, P. (eds.) Proceedings of the FLoC Workshop on Run-Time Result Verifiication, Trento, Italy (July 1999)
Shostak, R.: Deciding linear inequalities by computing loop residues. Journal of the ACM 28(4), 769–779 (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Necula, G.C., Lee, P. (2000). Proof Generation in the Touchstone Theorem Prover. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_3
Download citation
DOI: https://doi.org/10.1007/10721959_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive