Module `Logtk_proofs.LLProof`Source

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.

Sourceval section : Logtk.Util.Section.t

Sourcetype term = Logtk.TypedSTerm.t

Sourcetype ty = term

Sourcetype form = term

Sourcetype inst = term list

Instantiate some binder with the following terms. Order matters.

Sourcetype tag = Logtk.Proof.tag

Sourcetype name = string

Sourcetype t

Sourcetype 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;
}

Sourceand parent = {

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

Sourceval pp_step : step CCFormat.printer

Sourceval pp_parent : parent CCFormat.printer

Sourceval pp_id : t CCFormat.printer

Sourceval pp_res : t CCFormat.printer

Sourceval pp : t CCFormat.printer

Print only this step

Sourceval pp_dag : t CCFormat.printer

Print the whole DAG

Sourceval pp_inst : inst CCFormat.printer

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

Source

val inference : 
  intros:term list ->
  local_intros:term list ->
  tags:tag list ->
  form ->
  name ->
  parent list ->
  t

Checking steps

Sourcetype check_res =

| R_ok
| R_fail
| R_skip

Sourceval get_check_res : t -> check_res option

Sourceval set_check_res : t -> check_res -> unit

Sourceval pp_check_res : check_res CCFormat.printer

Printing

Sourcemodule Tbl : CCHashtbl.S with type key = t

Sourcemodule Dot : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Logtk_proofs.LLProof`Source

Low Level Proofs

Checking steps

Printing

package logtk

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Logtk_proofs.LLProofSource

Low Level Proofs

Checking steps

Printing

Module `Logtk_proofs.LLProof`Source