Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic

1. Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14(1), 3–19 (2004)

   Article  MATH  MathSciNet  Google Scholar 

2. Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 38–52. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

3. Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 24–40. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

4. Chaieb, A., Nipkow, T.: Generic proof synthesis for presburger arithmetic. Technical report, TU München (2003), http://www4.in.tum.de/~nipkow/pubs/presburger.pdf

5. Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 91–100. Edinburgh University Press (1972)

   Google Scholar 

6. Crégut, P.: Une procédure de décision réflexive pour un fragment de l’arithmétique de Presburger. In: Informal proceedings of the 15th journées francophones des langages applicatifs (2004)

   Google Scholar 

7. Fischer, M.J., Rabin, M.O.: Super-exponential complexity of presburger arithmetic. In: SIAMAMS: Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied Mathematics (1974)

   Google Scholar 

8. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Int. Conf. Functional Programming, pp. 235–246. ACM Press, New York (2002)

   Google Scholar 

9. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

10. Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), http://www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz

11. Harrison, J.: Theorem proving with the real numbers. PhD thesis, University of Cambridge, Computer Laboratory (1996)

    Google Scholar 

12. John Harrison’s home page, http://www.cl.cam.ac.uk/users/jrh/atp/OCaml/cooper.ml

13. Klapper, R., Stump, A.: Validated Proof-Producing Decision Procedures. In: Tinelli, C., Ranise, S. (eds.) 2nd Int. Workshop Pragmatics of Decision Procedures in Automated Reasoning (2004)

    Google Scholar 

14. Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

15. Norrish, M.: Complete integer decision procedures as derived rules in HOL. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 71–86. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

16. Oppen, D.C.: Elementary bounds for presburger arithmetic. In: STOC ’73: Proceedings of the fifth annual ACM symposium on Theory of computing, pp. 34–37. ACM Press, New York (1973)

    Chapter  Google Scholar 

17. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves, pp. 92–101 (1929)

    Google Scholar 

18. Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM/IEEE conference on Supercomputing, pp. 4–13. ACM Press, New York (1991)

    Chapter  Google Scholar 

19. Slind, K.: Derivation and use of induction schemes in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 275–290. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

Download references