package logtk

  1. Overview
  2. Docs
Core types and algorithms for logic

Install 

dune-project
 Dependency

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

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

1.6.tar.gz
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d

doc/logtk.proofs/Logtk_proofs/LLProof/index.html

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