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. © 2008 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Théry, L. (2008). Proof pearl: Revisiting the Mini-Rubik in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 310–319). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
