Functor Proofrule.Make

module Make: 
functor (Seq : Sigs.SEQUENT) -> Sigs.PROOFRULE 
  with type seq_t = Seq.t 
  with type proof_t = Proof.Make(Seq).t

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:

• a boolean eager
• a selection function s
• a matching function m The selection function is applied on the current subgoal and proof, and a list of goal indices is returned that represents possible back-link targets. This allows flexibility e.g., in changing from ancestral-only back-links to general ones.

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