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 3 years agoLinked 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 in Coq using optimization and theorem-proving techniques. | 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 | An algebraic combinatorics library formalized in Coq, providing a comprehensive set of functions and theories for symmetric functions. | 1 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 math-comp/coq-combi | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
| thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |