package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct