A Formally-Proven Algorithm for 2-Sat Problems

Laurent Théry 1, *
* Corresponding author
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This notes explains how an algorithm that checks the satisfiability of a set of two clause has been formalised in the Coq prover using the SSReflect extension.
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

Cited literature [4 references]  Display  Hide  Download
https://hal.inria.fr/hal-01095538
Contributor : Laurent Thery <>
Submitted on : Monday, December 15, 2014 - 5:25:14 PM
Last modification on : Thursday, January 11, 2018 - 4:22:42 PM
Document(s) archivé(s) le : Monday, March 16, 2015 - 12:30:24 PM

File

TwoSat.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01095538, version 1

Collections

INRIA | UNIV-COTEDAZUR

Citation

Laurent Théry. A Formally-Proven Algorithm for 2-Sat Problems. 2014. ⟨hal-01095538⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

123

Files downloads

93

Contact


archive-ouverte@inria.fr