package logtk

You can search for identifiers within the package.

in-package search v0.2.0

Core types and algorithms for logic

Install

Dune Dependency

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

Authors

Maintainers

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 =

| Goal
| Assert
| Negated_goal of t
| Trivial
| By_def of Logtk.ID.t
| Define of Logtk.ID.t
| Instantiate of {
1. form : t;
2. inst : inst;
3. tags : tag list;
}
| Esa of name * t list
| Inference of {
1. intros : term list;
2. local_intros : term list;
3. name : name;
4. parents : parent list;
5. tags : tag list;
}

and parent = {

p_proof : t;
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

val pp : 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 =

| R_ok
| R_fail
| 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

On This Page

Low Level Proofs
1. Checking steps
2. Printing