package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk_proofs.LLProof

Low Level Proofs

Low level proofs, intended for mechanical proof checking.

Instantiations (substitutions) are explicit because that should make the job of the checker easier.

NOTE: this is still uncooked, and will probably change.

val section : Logtk.Util.Section.t
type term = Logtk.TypedSTerm.t
type ty = term
type form = term
type inst = term list

Instantiate some binder with the following terms. Order matters.

type tag = Logtk.Proof.tag
type name = string
type t
type step =
  1. | Goal
  2. | Assert
  3. | Negated_goal of t
  4. | Trivial
  5. | By_def of Logtk.ID.t
  6. | Define of Logtk.ID.t
  7. | Instantiate of {
    1. form : t;
    2. inst : inst;
    3. tags : tag list;
    }
  8. | Esa of name * t list
  9. | Inference of {
    1. intros : term list;
    2. local_intros : term list;
    3. name : name;
    4. parents : parent list;
    5. tags : tag list;
    }
and parent = {
  1. p_proof : t;
  2. p_inst : inst;
}
val id : t -> int
val concl : t -> form
val step : t -> step
val parents : t -> parent list
val premises : t -> t list
val p_of : t -> parent
val p_inst : t -> inst -> parent
val pp_step : step CCFormat.printer
val pp_parent : parent CCFormat.printer
val pp_id : t CCFormat.printer
val pp_res : t CCFormat.printer

Print only this step

val pp_dag : t CCFormat.printer

Print the whole DAG

val pp_inst : inst CCFormat.printer
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val goal : form -> t
val negated_goal : form -> t -> t
val assert_ : form -> t
val trivial : form -> t
val by_def : Logtk.ID.t -> form -> t
val define : Logtk.ID.t -> form -> t
val instantiate : ?tags:tag list -> form -> t -> inst -> t
val esa : form -> name -> t list -> t
val inference : intros:term list -> local_intros:term list -> tags:tag list -> form -> name -> parent list -> t

Checking steps

type check_res =
  1. | R_ok
  2. | R_fail
  3. | R_skip
val get_check_res : t -> check_res option
val set_check_res : t -> check_res -> unit
val pp_check_res : check_res CCFormat.printer

Printing

module Tbl : CCHashtbl.S with type key = t
module Dot : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct