package logtk

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

Module Logtk_proofs.LLProofSource

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.

Sourcetype ty = term
Sourcetype form = term
Sourcetype inst = term list

Instantiate some binder with the following terms. Order matters.

Sourcetype name = string
Sourcetype t
Sourcetype 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;
    }
Sourceand parent = {
  1. p_proof : t;
  2. p_inst : inst;
}
Sourceval id : t -> int
Sourceval concl : t -> form
Sourceval step : t -> step
Sourceval parents : t -> parent list
Sourceval premises : t -> t list
Sourceval p_of : t -> parent
Sourceval p_inst : t -> inst -> parent

Print only this step

Print the whole DAG

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

Checking steps

Sourcetype check_res =
  1. | R_ok
  2. | R_fail
  3. | R_skip
Sourceval get_check_res : t -> check_res option
Sourceval set_check_res : t -> check_res -> unit

Printing

Sourcemodule Tbl : CCHashtbl.S with type key = t
Sourcemodule 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