Abstract
I describe the implementation of two complete decision procedures for integer Presburger arithmetic in the HOL theorem-proving system. The first procedure is Cooper’s algorithm, the second, the Omega Test. Between them, the algorithms illustrate three different implementation techniques in a fully expansive system.
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.
References
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.C., Giménez, E., Herbelin, H., Huet, G., Muñoz, C., Murthy, C., Parent, C., Paulin, C., Saïbi, A., Werner, B.: The Coq Proof Assistant Reference Manual – Version V6.1. Technical Report 0203, INRIA (August 1997), See the Coq home-page at http://coq.inria.fr/
Boulton, R.J.: Efficiency in a fully-expansive theorem prover. PhD thesis, Computer Laboratory, University of Cambridge (May 1994)
Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Machine Intelligence, New York, vol. 7, pp. 91–99. American Elsevier, Amsterdam (1972)
Gordon, M.J.C., Melham, T. (eds.): Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)
Harrison, J.: Theorem Proving with the Real Numbers. CPHC/BCS Distinguished Dissertations. Springer, Heidelberg (1998)
Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–321. Springer, Heidelberg (1999)
Jackson, P.B.: The Nuprl Proof Development System. Version 4.1 Reference Manual and User’s Guide. Cornell University, Ithaca (1994), See the Nuprl home-page at http://www.cs.cornell.edu/Info/Projects/NuPrl/html/NuprlSystem.html
Janičić, P., Green, I., Bundy, A.: A comparison of decision procedures in Presburger arithmetic. In: Proceedings of LIRA 1997: the 8th Conference on Logic and Computer Science, pp. 91–101. University of Novi Sad (1997); Also available as Research Paper 872, Department of AI. University of Edinburgh
Kaufmann, M., Moore, J.: An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering 23(4), 203–213 (1997)
Norrish, M., Slind, K.: A thread of HOL development. Computer Journal 45(1), 37–45 (2002)
Owre, S., Rushby, J., Shankar, N.: PVS:A PrototypeVerification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Pugh, W.: The Omega Test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM 35(8), 102–114 (1992)
Shostak, R.E.: On the SUP-INF method for proving Presburger formulas. Journal of the ACM 24(4), 529–543 (1977)
Shostak, R.E.: 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
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Norrish, M. (2003). Complete Integer Decision Procedures as Derived Rules in HOL. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_5
Download citation
DOI: https://doi.org/10.1007/10930755_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40664-8
Online ISBN: 978-3-540-45130-3
eBook Packages: Springer Book Archive