package msat

  1. Overview
  2. Docs

Module Msat_backend.CoqSource

Coq Backend

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

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule type Arg = sig ... end

Term printing for Coq

Sourcemodule 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

Sourcemodule 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

OCaml

Innovation. Community. Security.