minirubik
Rubik solver
Solves the mini Rubik 2x2 using theorem-proving in Coq
Solving the mini Rubik (2x2) in Coq
4 stars
2 watching
0 forks
Language: Coq
last commit: over 1 year ago
Linked from 1 awesome list
2x2x2coqformalizationrubik-cubetheorem-proving
Related projects:
| Repository | Description | Stars |
|---|---|---|
| thery/mathcomp-extra | A collection of reusable mathematical components and algorithms implemented in Coq | 5 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 coq-polyhedra/coq-polyhedra | Formalizes convex polyhedra using theorem-proving in Coq | 22 |
| thery/coqprime | A proof assistant library for prime number certification using elliptic curves and Pocklington certificates | 37 |
 coq-community/sudoku | A formalisation of Sudoku in Coq to solve the puzzle using a naive Davis-Putnam procedure | 20 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |
 acorrenson/saturne | A verified SAT solver with proof capabilities | 28 |
 wainwrightmark/puzzle_cube | A web-based solution for Rubik's cube puzzles, allowing users to solve and generate solve data in their browsers. | 9 |
 dmxlarchey/coq-kruskal | A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. | 0 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
| thery/flocqlecture | An introductory course on formalizing floating-point numbers and their applications in Coq | 6 |