Module Jst
module Jst: sig end
Justifications
Author(s): Harald Ruess
Every atom atm may have an associated justification rho; in this
case we also write rho |- atm. There are three different kinds of
ju1stifications
All justifies every- A set of dependencies
{atm1, ...,atmn}
- A proof skeleton (disabled in ICS 2.0)
Depending on the current proof mode, as obtained with Jst.Mode.get,
justifications of these kinds are generated.
module Mode: sig end
Proof Mode
type t
val pp : t Pretty.printer
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
j |
: |
Atom.Set.t
|
|
val axioms_of : t -> Atom.Set.t
val of_axioms : Atom.Set.t -> t
exception Inconsistent of t
val axiom : Atom.t -> t
val dep0 : t
val dep1 : t -> t
val dep2 : t -> t -> t
val dep3 : t -> t -> t -> t
val dep4 : t -> t -> t -> t -> t
| Parameters: |
|
j1 |
: |
t
|
|
j2 |
: |
t
|
|
j3 |
: |
t
|
|
j4 |
: |
t
|
|
val dep5 : t -> t -> t -> t -> t -> t
| Parameters: |
|
j1 |
: |
t
|
|
j2 |
: |
t
|
|
j3 |
: |
t
|
|
j4 |
: |
t
|
|
j5 |
: |
t
|
|
val dep : t list -> t
type jst = t
Nickname.
module Three: sig end
Justifying ternary relations.
module Eqtrans: sig end
Justifying equality Transformers
module Pred: sig end
Justifying predicates over terms.
module Pred2: sig end
Justifying predicates over pair of terms.
module Rel1: sig end
Justifying ternary relations over terms.
module Rel2: sig end
Justifying ternary relations over pairs of terms.