package mc2

  1. Overview
  2. Docs

Dot backend for proofs

This module provides functions to export proofs into the dot graph format. Graphs in dot format can be used to generates images using the graphviz tool.

module type S = Backend_intf.S

Interface for exporting proofs.

module type Arg = sig ... end

Term printing for DOT

module Default : Arg with type atom := Mc2_core.Atom.t and type hyp := Mc2_core.Clause.t and type lemma := Mc2_core.Clause.t and type assumption := Mc2_core.Clause.t

Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.

module Make (A : Arg with type atom := Mc2_core.Atom.t and type hyp := Mc2_core.Clause.t and type lemma := Mc2_core.Clause.t and type assumption := Mc2_core.Clause.t) : S with type t := Mc2_core.Proof.t

Functor for making a module to export proofs to the DOT format.