Skip to main content
SpringerLink
Log in

Proof Pearl: Revisiting the Mini-rubik in Coq

  • Conference paper
Theorem Proving in Higher Order Logics (TPHOLs 2008)

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

Included in the following conference series:

Abstract

The Mini-Rubik is the 2x2x2 version of the famous Rubik’s cube. How many moves are required to solve the 3x3x3 cube is still unknown. The Mini-Rubik, being simpler, is always solvable in a maximum of 11 moves. This is the result that is formalised in this paper. From this formalisation, a solver is also derived inside the Coq prover. This rather simple example illustrates how safe computation can be used to do state exploration in order to derive non-trivial properties inside a prover.

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. Cooperman, G., Finkelstein, L.: New Methods for Using Cayley Graphs in Interconnection Networks. Discrete Applied Mathematics 37(38), 95–118 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  2. Frey, A.H., Singmaster, D.: Handbook of Cubik Math. Enslow Publishers (1982)

    Google Scholar 

  3. Gordon, M.J.C.: Reachability Programming in HOL98 using BDDs. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 179–196. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Michael J. C. Gordon and Thomas F. Melham. Introduction to HOL : a theorem proving environment for higher-order logic. Cambridge University Press, 1993.

    MATH  Google Scholar 

  5. Kunkle, D., Cooperman, G.: Twenty-Six Moves Suffice for Rubik’s Cube. In: ISSAC 2007, pp. 235–242 (2007)

    Google Scholar 

  6. Leroy, X.: Objective Caml (1997), http://pauillac.inria.fr/ocaml/

  7. Spiwack, A.: Efficient Integer Computation in Type Theory, Draft paper (2007)

    Google Scholar 

  8. The Coq development team. The Coq Proof Assistant Reference Manual v7.2. Technical Report 255, INRIA (2002), http://coq.inria.fr/doc

  9. Théry, L., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 319–333. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Valmari, A.: What the small Rubik’s cube taught me about data structures, information theory, and randomisation. International Journal for Software Tools Technology 8(3), 180–194 (2006)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Marelle Project INRIA, France

    Laurent Théry

Authors
  1. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve Blvd. W, H3G 1M8, Montreal, Quebec, Canada

    Otmane Ait Mohamed

  2. National Institute of Aerospace, 100 Exploration Way, VA 23666, Hampton, USA

    César Muñoz

  3. Dept. of Electrical & Computer Engineering, Concordia University, 1455 de Maisonette W, H3G 1M8, Montreal, Quebec, Canada

    Sofiène Tahar

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Théry, L. (2008). Proof Pearl: Revisiting the Mini-rubik in Coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2008. Lecture Notes in Computer Science, vol 5170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71067-7_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-71067-7_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-71065-3

  • Online ISBN: 978-3-540-71067-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation