Module Proof

module Proof: sig .. end

Manipulate proofs

module Loc: Logtk.ParseLocation

type form = Logtk.TypedSTerm.t

type bool_lit = BBox.Lit.t

type 'a sequence = ('a -> unit) -> unit

val section : Logtk.Util.Section.t

type statement_src = Logtk.Statement.source

type rule

type check = [ `Check | `Check_with of form list | `No_check ]

How do we check a step?

type kind =

`\|`	`Inference of rule * check`
`\|`	`Simplification of rule * check`
`\|`	`Esa of rule * check`
`\|`	`Assert of statement_src`
`\|`	`Goal of statement_src`
`\|`	`Lemma`
`\|`	`Data of statement_src * Logtk.Type.t Logtk.Statement.data`
`\|`	`Trivial`	`(*`	trivial, or trivial within theories	`*)`
`\|`	`By_def of Logtk.ID.t`

Classification of proof steps

type result =

`\|`	`Form of form`
`\|`	`Clause of SClause.t`
`\|`	`BoolClause of bool_lit list`
`\|`	`Stmt of Logtk.Statement.input_t`
`\|`	`C_stmt of Logtk.Statement.clause_t`

type step

A proof step, without the conclusion

type proof

Proof Step with its conclusion

type t = proof

type parent

type info = Logtk.UntypedAST.attr

type infos = info list

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

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 Proof.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

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