package orthologic-coq

  1. Overview
  2. Docs
A plugin to add orthologic-based tactics to Coq

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

  1. S
    Simon Guilloud
  2. C
    Clément Pit-Claudel

Maintainers

  1. S
    Simon Guilloud

Sources

orthologic-coq-0.9.1.tbz
sha256=60a9eeb27b6ad0a6fadb4127f5a7fdc194133dc55fa627e5eaedbee58a58651e
sha512=bab767857cecbb1529e599785f2485e62171a55b7ec34483976a9a15e8223167c52a2977f88752e64f17fd1b4e6fde682b608bd046b2a7867da2eca10844cf57

doc/orthologic-coq.plugin/OLCoq/Ol/index.html

Module OLCoq.OlSource

Sourceval total_formula : int ref
Sourceval total_polar : int ref
Sourceval total_normal : int ref
Sourcetype formula =
  1. | Variable of {
    1. id : int;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  2. | Neg of {
    1. child : formula;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  3. | Or of {
    1. children : formula list;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  4. | And of {
    1. children : formula list;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  5. | Literal of {
    1. b : bool;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
Sourceand polar_formula =
  1. | PolarVariable of {
    1. id : int;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : polar_formula option;
    5. mutable normal_form : normal_formula option;
    }
  2. | PolarAnd of {
    1. children : polar_formula list;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : polar_formula option;
    5. mutable normal_form : normal_formula option;
    }
  3. | PolarLiteral of {
    1. b : bool;
    2. unique_key : int;
    3. mutable inverse : polar_formula option;
    4. mutable normal_form : normal_formula option;
    }
Sourceand normal_formula =
  1. | NormalVariable of {
    1. id : int;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : normal_formula option;
    5. mutable formulaP : formula option;
    6. mutable formulaN : formula option;
    7. lt_cache : (int, bool) Hashtbl.t;
    }
  2. | NormalAnd of {
    1. children : normal_formula list;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : normal_formula option;
    5. mutable formulaP : formula option;
    6. mutable formulaN : formula option;
    7. lt_cache : (int, bool) Hashtbl.t;
    }
  3. | NormalLiteral of {
    1. b : bool;
    2. unique_key : int;
    3. mutable inverse : normal_formula option;
    4. mutable formulaP : formula option;
    5. mutable formulaN : formula option;
    6. lt_cache : (int, bool) Hashtbl.t;
    }
Sourceval new_variable : int -> formula
Sourceval new_neg : formula -> formula
Sourceval new_or : formula list -> formula
Sourceval new_and : formula list -> formula
Sourceval new_literal : bool -> formula
Sourceval new_p_variable : int -> bool -> polar_formula
Sourceval new_p_and : polar_formula list -> bool -> polar_formula
Sourceval new_p_literal : bool -> polar_formula
Sourceval new_n_variable : int -> bool -> normal_formula
Sourceval new_n_and : normal_formula list -> bool -> normal_formula
Sourceval new_n_literal : bool -> normal_formula
Sourceval get_key : formula -> int
Sourceval get_polar_formula : formula -> polar_formula option
Sourceval set_polar_formula : formula -> polar_formula option -> unit
Sourceval get_p_normal_form : polar_formula -> normal_formula option
Sourceval set_p_normal_form : polar_formula -> normal_formula option -> unit
Sourceval size : formula -> int
Sourceval get_p_key : polar_formula -> int
Sourceval get_p_inverse_option : polar_formula -> polar_formula option
Sourceval set_p_inverse_option : polar_formula -> polar_formula option -> unit
Sourceval get_n_key : normal_formula -> int
Sourceval get_n_inverse_option : normal_formula -> normal_formula option
Sourceval set_n_inverse_option : normal_formula -> normal_formula option -> unit
Sourceval get_formulaP : normal_formula -> formula option
Sourceval set_formulaP : normal_formula -> formula option -> unit
Sourceval get_formulaN : normal_formula -> formula option
Sourceval set_formulaN : normal_formula -> formula option -> unit
Sourceval get_lt_cache : normal_formula -> (int, bool) Hashtbl.t
Sourceval lt_cached : normal_formula -> normal_formula -> bool option
Sourceval set_lt_cached : normal_formula -> normal_formula -> bool -> unit
Sourceval formula_to_string : formula -> string
Sourceval polar_formula_to_string : polar_formula -> string
Sourceval normal_formula_to_string : normal_formula -> string
Sourceval get_polar_inverse : polar_formula -> polar_formula
Sourceval polarize : formula -> bool -> polar_formula
Sourceval get_normal_inverse : normal_formula -> normal_formula
Sourceval to_formula_nnf : normal_formula -> bool -> formula
Sourceval to_formula : normal_formula -> formula
Sourceval lattices_leq : normal_formula -> normal_formula -> bool
Sourceval simplify : normal_formula list -> bool -> normal_formula
Sourceval check_for_contradiction : normal_formula -> bool
Sourceval polar_to_normal_form : polar_formula -> normal_formula
Sourceval reduced_form : formula -> formula
Sourceval show_ol : unit -> unit