A Formally-Proven Algorithm for 2-Sat Problems

Laurent Théry 1, *
* Auteur correspondant
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.
Type de document :
Pré-publication, Document de travail
2014
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01095538
Contributeur : Laurent Thery <>
Soumis le : lundi 15 décembre 2014 - 17:25:14
Dernière modification le : jeudi 11 janvier 2018 - 16:22:42
Document(s) archivé(s) le : lundi 16 mars 2015 - 12:30:24

Fichier

TwoSat.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01095538, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

87