Module type Sigs.PROOFRULE

module type PROOFRULE = sig .. end

type seq_t 
type proof_t 
type axiom_f = seq_t -> string option 
type infrule_app = (seq_t * Tagpairs.t * Tagpairs.t) list * string 
type infrule_f = seq_t -> infrule_app list 
type backrule_f = seq_t -> seq_t -> (Tagpairs.t * string) list 
type select_f = int -> proof_t -> int list 
type t = int -> proof_t -> (int list * proof_t) Blist.t 
The type of proof rules: Proof rules are functions that take an open node in a proof (i.e. an int identifying the node, and the proof structure containing the node) and return a list of new proofs that are obtained by applying the rule in all applicable ways to the open node in the provided proof, along with a list for each new proof of the newly added open nodes (i.e. the premises) *
val mk_axiom : axiom_f -> t
Axioms are modeled as functions that return Some string when the input sequent is an instance of an axiom described by string, else None.
val mk_infrule : infrule_f -> t
Rules are functions that break down a sequent to a choice of applications where each application is a list of premises, including tag information, and a description.
val mk_backrule : bool ->
select_f -> backrule_f -> t
Backlink rules take: Next, m is applied to every pair consisting of the current subgoal and a goal returned from the selection function. m returns a list of tag information and string descriptions, each describing a different way to form a back-link.

If eager is true then the first result in this iteration will be chosen and no back-tracking will even happen over later possible matches. Otherwise all possible matches are returned as different choices.

val all_nodes : select_f
Ready-made selection functions doing the obvious.
val closed_nodes : select_f
val ancestor_nodes : select_f
val syntactically_equal_nodes : select_f
val fail : t
The rule that always fails.

Return current subgoal and proof as application.

val identity : t
val attempt : t -> t
Try a rule and if it fails act as identity.

Apply the second rule on all premises generated by applying the first.

val compose : t -> t -> t
Apply the list of rules in the second argument in a pairwise fashion to the premises generated by applying the first rule
val compose_pairwise : t -> t list -> t
val choice : t list -> t
Apply a list of rules on current subgoal and return all applications.

Try rules from a list until the first rule is found that has some applications on current sugboal and return only those.

val first : t list -> t
Apply a sequence of rules iteratively through compose.
val sequence : t list -> t
val conditional : (seq_t -> bool) -> t -> t
val combine_axioms : t -> t -> t