package msat

  1. Overview
  2. Docs

Coq Backend

This module provides an easy way to produce coq scripts corresponding to the resolution proofs output by the sat solver.

module type S = Backend_intf.S

Interface for exporting proofs.

module type Arg = sig ... end

Term printing for Coq

module Make (S : Msat.S) (A : Arg with type hyp := S.clause and type lemma := S.clause and type assumption := S.clause) : S with type t := S.proof

Base functor to output Coq proofs

module Simple (S : Msat.S) (A : Arg with type hyp = S.formula list and type lemma := S.lemma and type assumption := S.formula) : S with type t := S.proof

Simple functor to output Coq proofs