Sudoku in Coq
Sudoku en Coq
Résumé
This note presents a formalisation done in Coq of Sudoku. We formalise what is a Sudoku, a Sudoku checker and a Sudoku solver. The Sudoku solver uses a naive Davis-Putnam procedure.
Cette note présente une formalisation en Coq du Sudoku. Nous formalisons ce qu'est un vérificateur de Sudoku et un solveur de Sudoku. Le solveur de Sudoku utilise une procédure naïve de Davis-Putnam,
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)