Core types and algorithms for logic
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(*


| 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


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.


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

Proof Results

A proof is used to deduce some results. We can handle diverse results a different stages of the proof (starting with formulas, ending with clauses)

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.


The link between a proof step and some intermediate results used to prove its result

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


A proof is a pair of a result, with its proof step. Typically, a refutation will be a proof of false from axioms and the negated goal.

module S : sig ... end