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 =
  1. | Intro of source * role
  2. | Inference of rule * tag list
  3. | Simplification of rule * tag list
  4. | Esa of rule
  5. | Trivial
    (*

    trivial, or trivial within theories

    *)
  6. | Define of ID.t * source
    (*

    definition

    *)
  7. | By_def of ID.t
    (*

    following from the def of ID

    *)

Classification of proof steps

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

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

and source_view =
  1. | From_file of from_file * attrs
  2. | Internal of attrs
and role =
  1. | R_assert
  2. | R_goal
  3. | R_def
  4. | R_decl
  5. | R_lemma

Intro role

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

Typeclass for the result of a proof step

type result =
  1. | 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 =
  1. | P_of of t
  2. | 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

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.

Parent

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

Proof

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