Skip to main content
SpringerLink
Log in

Fast Reflexive Arithmetic Tactics the Linear Case and Beyond

  • Conference paper
Book cover Types for Proofs and Programs (TYPES 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4502))

Included in the following conference series:

Abstract

When goals fall in decidable logic fragments, users of proof-assistants expect automation. However, despite the availability of decision procedures, automation does not come for free. The reason is that decision procedures do not generate proof terms. In this paper, we show how to design efficient and lightweight reflexive tactics for a hierarchy of quantifier-free fragments of integer arithmetics. The tactics can cope with a wide class of linear and non-linear goals. For each logic fragment, off-the-shelf algorithms generate certificates of infeasibility that are then validated by straightforward reflexive checkers proved correct inside the proof-assistant. This approach has been prototyped using the Coq proof-assistant. Preliminary experiments are promising as the tactics run fast and produce small proof terms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bellman, R.: On a routing problem. In Quarterly of Applied Mathematics 16, 87–90 (1958)

    MATH  Google Scholar 

  2. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Coq’Art: the Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  3. Besson, F., Jensen, T., Pichardie, D.: A PCC Architecture based on Certified Abstract Interpretation. In: Proc. of 1st Int. Workshop on Emerging Applications of Abstract Interpretation, ENTCS, Springer, Heidelberg (2006)

    Google Scholar 

  4. Besson, F., Jensen, T., Pichardie, D.: Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression. Theoretical Computer Science 364, 273–291 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  5. Borchers, B.: Csdp, 2.3 user’s guide. Optimization Methods and Software 11(2), 597–611 (1999)

    Article  MathSciNet  Google Scholar 

  6. Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342(1), 56–78 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  7. Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 367–380. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Crégut, P.: Une procédure de décision réflexive pour un fragment de l’arithmétique de presburger. In Journées Francophones des Langages Applicatifs (2004)

    Google Scholar 

  9. The Coq development team: The coq proof assistant - reference manual v 8.1

    Google Scholar 

  10. Déharbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: 1st IEEE Int. Conf. on Software Engineering and Formal Methods, IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  11. Fontaine, P., Marion, J-Y., Merz, S., Nieto, L., Tiu, A.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

    Google Scholar 

  13. 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)

    Google Scholar 

  14. Grégoire, B., Théry, L., Werner, B.: A computational approach to pocklington certificates in type theory. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 97–113. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Harrison, J.: HOL light tutorial (for version 2.20)

    Google Scholar 

  16. Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. Journal of Automated Reasoning 21, 279–294 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  17. Karmarkar, N.: A new polynomial-time algorithm for linear programming. In: Proc. of the 16th ACM Symp. on Theory of Computing, pp. 302–311. ACM Press, New York (1984)

    Google Scholar 

  18. Necula, G.: Proof-carrying code. In: Proc. of the 24th ACM Symp. on Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)

    Google Scholar 

  19. Obua, S.: Proving bounds for real linear programs in isabelle/hol. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 227–244. Springer, Heidelberg (2005)

    Google Scholar 

  20. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  21. Pratt, V.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology (1977)

    Google Scholar 

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

    Chapter  Google Scholar 

  23. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1998)

    MATH  Google Scholar 

  24. Shostak, R.: Deciding linear inequalities by computing loop residues. J. ACM 28(4), 769–779 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  25. Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Mathematische Annalen 207(2), 87–97 (1973)

    Article  MATH  MathSciNet  Google Scholar 

  26. Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press (1951)

    Google Scholar 

  27. Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49–95 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  28. Weber, T.: Using a SAT solver as a fast decision procedure for propositional logic in an LCF-style theorem prover. In: Proc. of 18th Int. Conf. on the Theorem Proving in Higher Order Logics, pp. 180–189 (August 2005)

    Google Scholar 

  29. Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe, pp. 10880–10885. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Irisa/Inria, Campus de Beaulieu, 35042 Rennes Cedex, France

    Frédéric Besson

Authors
  1. Frédéric Besson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Thorsten Altenkirch Conor McBride

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Besson, F. (2007). Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: Altenkirch, T., McBride, C. (eds) Types for Proofs and Programs. TYPES 2006. Lecture Notes in Computer Science, vol 4502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74464-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74464-1_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74463-4

  • Online ISBN: 978-3-540-74464-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation