Skip to Main content Skip to Navigation
Reports

Sudoku in Coq

Laurent Théry 1 
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/hal-03277886
Contributor : Laurent Théry Connect in order to contact the contributor
Submitted on : Monday, July 5, 2021 - 10:38:59 AM
Last modification on : Saturday, June 25, 2022 - 11:51:00 PM
Long-term archiving on: : Wednesday, October 6, 2021 - 6:12:33 PM

File

Note.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03277886, version 1

Collections

Citation

Laurent Théry. Sudoku in Coq. [Research Report] INRIA Sophia Antipolis - Méditerranée. 2006. ⟨hal-03277886⟩

Share

Metrics

Record views

74

Files downloads

44