A Formally-Proven Algorithm for 2-Sat Problems - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

A Formally-Proven Algorithm for 2-Sat Problems

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

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.

Domains

Computer Science [cs] Logic in Computer Science [cs.LO]
Fichier principal
Vignette du fichier
TwoSat.pdf (131.54 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Laurent Théry  : Connect in order to contact the contributor

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

Submitted on : Monday, December 15, 2014-5:25:14 PM

Last modification on : Saturday, June 25, 2022-11:15:31 PM

Long-term archiving on: Monday, March 16, 2015-12:30:24 PM

Download

Dates and versions

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

Identifiers

  • HAL Id : hal-01095538 , version 1

Cite

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

Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

Collections

INRIA INRIA2
74 View
64 Download

Share

Gmail Facebook Twitter LinkedIn More