#### logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module .

## 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

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`