Module Logtk.Proof

Manipulate proofs

module Loc = ParseLocation
type term = TypedSTerm.t
type form = TypedSTerm.t
type 'a sequence = ('a -> unit) -> unit
val section : Util.Section.t
type rule
type tag = Builtin.Tag.t

Tag for checking an inference. Each tag describes an extension of FO that is used in the inference

type attrs = UntypedAST.attrs
type kind =
| Intro of source * role
| Inference of rule * tag list
| Simplification of rule * tag list
| Esa of rule
| Trivial

trivial, or trivial within theories

| Define of ID.t * source

definition

| By_def of ID.t

following from the def of ID

Classification of proof steps

and source = private {
src_id : int;
src_view : source_view;
}

Source of leaves (from some input problem, or internal def)

and source_view =
| From_file of from_file * attrs
| Internal of attrs
and role =
| R_assert
| R_goal
| R_def
| R_decl
| R_lemma

Intro role

and from_file = {
file : string;
name : string option;
loc : ParseLocation.t option;
}
type 'a result_tc

Typeclass for the result of a proof step

type result =
| Res : 'a result_tc * exn -> result

result of an inference

type step

A proof step, without the conclusion

type proof

Proof Step with its conclusion

type t = proof
type parent =
| P_of of t
| P_subst of t * Subst.Projection.t
type info = UntypedAST.attr
type infos = info list
module Tag = Builtin.Tag

Rule

module Rule : sig ... end

A rule is a name for some specific inference or transformation rule that is used to deduce formulas from other formulas.

Kind

module Kind : sig ... end
module Src : sig ... end

Proof Results

module Result : sig ... end

A proof step

module Step : sig ... end

An inference step is composed of a set of premises, a rule, a status (theorem/trivial/equisatisfiable…), and is used to deduce new result using these premises and metadata.

Parent

module Parent : sig ... end
val pp_parent : Parent.t CCFormat.printer
val pp_tag : tag CCFormat.printer
val pp_tags : tag list CCFormat.printer

Proof

module S : sig ... end