A Formally-Proven Algorithm for 2-Sat Problems
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.
Origin : Files produced by the author(s)
Loading...