Implicational Rewriting Tactics in HOL | SpringerLink
Skip to main content
Springer Nature Link
Log in

Implicational Rewriting Tactics in HOL

  • Conference paper
Interactive Theorem Proving (ITP 2014)

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

Included in the following conference series:

  • 993 Accesses

Abstract

Reducing the distance between informal and formal proofs in interactive theorem proving is a long-standing matter. An approach to this general topic is to increase automation in theorem provers: indeed, automation turns many small formal steps into one big step. In spite of the usual automation methods, there are still many situations where the user has to provide some information manually, whereas this information could be derived from the context. In this paper, we characterize some very common use cases where such situations happen, and identify some general patterns behind them. We then provide solutions to deal with these situations automatically, which we implemented as HOL Light and HOL4 tactics. We find these tactics to be extremely useful in practice, both for their automation and for the feedback they provide to the user.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

  1. Aravantinos, V.: Implicational Conversions for HOL Light and HOL4 (2013), https://github.com/aravantv/impconv , https://github.com/aravantv/impconv/HOL4-impconv (respectively)

  2. Asperti, A., Tassi, E.: Smart Matching. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC/Calculemus/MKM 2010. LNCS (LNAI), vol. 6167, pp. 263–277. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)

    Google Scholar 

  4. Bachmair, L., Ganzinger, H.: Rewrite-Based Equational Theorem Proving with Selection and Simplification. Journal of Logical Computation 4(3), 217–247 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  5. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press (2009)

    Google Scholar 

  6. Braibant, T., Pous, D.: Tactics for Reasoning Modulo AC in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 167–182. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Brünnler, K., Tiu, A.F.: A Local System for Classical Logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347–361. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Cooper, D.C.: Theorem Proving in Arithmetic Without Multiplication. Machine Intelligence 7, 91–99 (1972)

    MATH  Google Scholar 

  9. Brand, D., Darringer, J., Joyner, W.: Completeness of Conditional Reductions. Research Report RC-7404, IBM (1978)

    Google Scholar 

  10. Davis, M., Logemann, G., Loveland, D.W.: A Machine Program for Theorem-Proving. Communications of the ACM 5(7), 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  11. Dowek, G., Hardin, T., Kirchner, C.: Theorem Proving Modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  12. Fitting, M.: First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer (1990)

    Google Scholar 

  13. Gonthier, G., Tassi, E.: A Language of Patterns for Subterm Selection. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 361–376. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. Harrison, J.: The HOL Light System Reference (2013), http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.html

  15. Homeier, P.V.: HOL4 source code (2002), http://ww.src/1/dep_rewrite.sml

  16. Huet, G.P.: A Mechanization of Type Theory. In: International Joint Conference on Artificial Intelligence, pp. 139–146. William Kaufmann (1973)

    Google Scholar 

  17. Inverardi, P.: Rewriting for preorder relations. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 223–234. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  18. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series. Springer (2008)

    Google Scholar 

  19. Liu, L., Hasan, O., Aravantinos, V., Tahar, S.: Formal Reasoning about Classified Markov Chains in HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 295–310. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 413–427. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Mayr, R., Nipkow, T.: Higher-Order Rewrite Systems and Their Confluence. Theoretical Computer Science 192(1), 3–29 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  22. Norrish, M.: Rewriting Conversions Implemented with Continuations. Journal of Automated Reasoning 43(3), 305–336 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  23. Paulson, L.C.: A Higher-Order Implementation of Rewriting. Science of Computer Programming 3(2), 119–149 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  24. Paulson, L.C., Blanchette, J.C.: Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In: IWIL@LPAR. EPiC Series, vol. 2, pp. 1–11 (2010)

    Google Scholar 

  25. Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press (2001)

    Google Scholar 

  26. Robinson, P.J., Staples, J.: Formalizing a Hierarchical Structure of Practical Mathematical Reasoning. Journal of Logical Computation 3(1), 47–61 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  27. Siddique, U., Aravantinos, V., Tahar, S.: Formal Stability Analysis of Optical Resonators. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 368–382. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  28. Slind, K.: AC Unification in HOL90. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 436–449. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  29. Slind, K., Norrish, M.: A Brief Overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  30. Solovyev, A.: SSReflect/HOL Light manual. Flyspeck project (2012)

    Google Scholar 

  31. Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A Tool for Proof Re-animation. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC/Calculemus/MKM 2010. LNCS (LNAI), vol. 6167, pp. 440–454. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  32. Türk, T.: HOL4 source code (2006)

    Google Scholar 

  33. Türk, T.: HOL4 source code (2008), http://src/1/ConseqConv.sml

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software & Systems Engineering, Fortiss GmbH, Guerickestraße 25, 80805, Munich, Germany

    Vincent Aravantinos

  2. Electrical and Computer Engineering Dept., Concordia University, 1455 De Maisonneuve Blvd. W., Montreal, Canada

    Sofiène Tahar

Authors
  1. Vincent Aravantinos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sofiène Tahar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NICTA, Sydney, NSW, Australia

    Gerwin Klein

  2. University of Wyoming, Laramie, WY, USA

    Ruben Gamboa

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Aravantinos, V., Tahar, S. (2014). Implicational Rewriting Tactics in HOL. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08970-6_4

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08969-0

  • Online ISBN: 978-3-319-08970-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation