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 =
Classification of proof steps
type
result =
type
step
A proof step, without the conclusion
type
proof
Proof Step with its conclusion
type
t = proof
type
parent
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