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.2.17@m4x.org

Sources

2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

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

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