A Formally-Proven Algorithm for 2-Sat Problems - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2014

A Formally-Proven Algorithm for 2-Sat Problems

Laurent Théry
Connectez-vous pour contacter l'auteur
Mathematical, Reasoning and Software

Résumé

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.

Domaines

Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
TwoSat.pdf (131.54 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Laurent Théry  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/hal-01095538

Soumis le : lundi 15 décembre 2014-17:25:14

Dernière modification le : mercredi 15 mars 2023-08:58:09

Archivage à long terme le : lundi 16 mars 2015-12:30:24

Télécharger pour visualiser

Dates et versions

hal-01095538 , version 1 (15-12-2014)

Identifiants

  • HAL Id : hal-01095538 , version 1

Citer

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

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

INRIA INRIA2
79 Consultations
85 Téléchargements

Partager

Gmail Facebook X LinkedIn More