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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bellman, R.: On a routing problem. In Quarterly of Applied Mathematics 16, 87–90 (1958)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Coq’Art: the Calculus of Inductive Constructions. Springer, Heidelberg (2004)
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)
Besson, F., Jensen, T., Pichardie, D.: Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression. Theoretical Computer Science 364, 273–291 (2006)
Borchers, B.: Csdp, 2.3 user’s guide. Optimization Methods and Software 11(2), 597–611 (1999)
Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342(1), 56–78 (2005)
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)
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)
The Coq development team: The coq proof assistant - reference manual v 8.1
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)
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)
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)
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)
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)
Harrison, J.: HOL light tutorial (for version 2.20)
Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. Journal of Automated Reasoning 21, 279–294 (1998)
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)
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)
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)
Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)
Pratt, V.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology (1977)
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)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1998)
Shostak, R.: Deciding linear inequalities by computing loop residues. J. ACM 28(4), 769–779 (1981)
Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Mathematische Annalen 207(2), 87–97 (1973)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press (1951)
Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49–95 (1996)
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)
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)
Author information
Authors and Affiliations
Editor information
Rights 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)