sig
  module type SEQUENT =
    sig
      type t
      val equal : Sigs.SEQUENT.t -> Sigs.SEQUENT.t -> bool
      val equal_upto_tags : Sigs.SEQUENT.t -> Sigs.SEQUENT.t -> bool
      val tags : Sigs.SEQUENT.t -> Tags.t
      val to_string : Sigs.SEQUENT.t -> string
      val to_melt : Sigs.SEQUENT.t -> Latex.t
      val pp : Format.formatter -> Sigs.SEQUENT.t -> unit
    end
  module type DEFS =
    sig
      type t
      val to_string : Sigs.DEFS.t -> string
      val to_melt : Sigs.DEFS.t -> Latex.t
      val pp : Format.formatter -> Sigs.DEFS.t -> unit
    end
  module type NODE =
    sig
      type t
      type seq_t
      val mk_open : Sigs.NODE.seq_t -> Sigs.NODE.t
      val mk_axiom : Sigs.NODE.seq_t -> string -> Sigs.NODE.t
      val mk_backlink :
        Sigs.NODE.seq_t -> string -> int -> Tagpairs.t -> Sigs.NODE.t
      val mk_inf :
        Sigs.NODE.seq_t ->
        string -> (int * Tagpairs.t * Tagpairs.t) list -> Sigs.NODE.t
      val dest : Sigs.NODE.t -> Sigs.NODE.seq_t * string
      val dest_backlink :
        Sigs.NODE.t -> Sigs.NODE.seq_t * string * int * Tagpairs.t
      val dest_inf :
        Sigs.NODE.t ->
        Sigs.NODE.seq_t * string * (int * Tagpairs.t * Tagpairs.t) list
      val is_open : Sigs.NODE.t -> bool
      val is_axiom : Sigs.NODE.t -> bool
      val is_backlink : Sigs.NODE.t -> bool
      val is_inf : Sigs.NODE.t -> bool
      val get_seq : Sigs.NODE.t -> Sigs.NODE.seq_t
      val get_succs : Sigs.NODE.t -> int list
      val to_abstract_node : Sigs.NODE.t -> Soundcheck.abstract_node
      val pp : Format.formatter -> Sigs.NODE.t -> unit
      val to_melt :
        bool -> int -> Sigs.NODE.t -> (bool -> int -> Latex.t) -> Latex.t
    end
  module type PROOF =
    sig
      type t
      type seq_t
      type node_t
      val mk : Sigs.PROOF.seq_t -> Sigs.PROOF.t
      val add_axiom : int -> string -> Sigs.PROOF.t -> Sigs.PROOF.t
      val add_backlink :
        int -> string -> int -> Tagpairs.t -> Sigs.PROOF.t -> Sigs.PROOF.t
      val add_inf :
        int ->
        string ->
        (Sigs.PROOF.seq_t * Tagpairs.t * Tagpairs.t) list ->
        Sigs.PROOF.t -> int list * Sigs.PROOF.t
      val add_subprf : Sigs.PROOF.t -> int -> Sigs.PROOF.t -> Sigs.PROOF.t
      val extract_subproof : int -> Sigs.PROOF.t -> Sigs.PROOF.t
      val find : int -> Sigs.PROOF.t -> Sigs.PROOF.node_t
      val get_seq : int -> Sigs.PROOF.t -> Sigs.PROOF.seq_t
      val size : Sigs.PROOF.t -> int
      val num_backlinks : Sigs.PROOF.t -> int
      val fresh_idx : Sigs.PROOF.t -> int
      val fresh_idxs : 'a list -> Sigs.PROOF.t -> int list
      val get_ancestry :
        int -> Sigs.PROOF.t -> (int * Sigs.PROOF.node_t) list
      val is_closed_at : Sigs.PROOF.t -> int -> bool
      val check : Sigs.PROOF.t -> bool
      val is_closed : Sigs.PROOF.t -> bool
      val to_list : Sigs.PROOF.t -> (int * Sigs.PROOF.node_t) list
      val pp : Format.formatter -> Sigs.PROOF.t -> unit
      val to_string : Sigs.PROOF.t -> string
      val to_melt : Sigs.PROOF.t -> Latex.t
    end
  module type SEQTACTICS =
    sig
      type seq_t
      type ruleapp_t =
          (Sigs.SEQTACTICS.seq_t * Tagpairs.t * Tagpairs.t) list * string
      type t = Sigs.SEQTACTICS.seq_t -> Sigs.SEQTACTICS.ruleapp_t list
      val relabel : string -> Sigs.SEQTACTICS.t -> Sigs.SEQTACTICS.t
      val attempt : Sigs.SEQTACTICS.t -> Sigs.SEQTACTICS.t
      val compose :
        Sigs.SEQTACTICS.t -> Sigs.SEQTACTICS.t -> Sigs.SEQTACTICS.t
      val first : Sigs.SEQTACTICS.t list -> Sigs.SEQTACTICS.t
      val repeat : Sigs.SEQTACTICS.t -> Sigs.SEQTACTICS.t
      val choice : Sigs.SEQTACTICS.t list -> Sigs.SEQTACTICS.t
    end
  module type PROOFRULE =
    sig
      type seq_t
      type proof_t
      type axiom_f = Sigs.PROOFRULE.seq_t -> string option
      type infrule_app =
          (Sigs.PROOFRULE.seq_t * Tagpairs.t * Tagpairs.t) list * string
      type infrule_f =
          Sigs.PROOFRULE.seq_t -> Sigs.PROOFRULE.infrule_app list
      type backrule_f =
          Sigs.PROOFRULE.seq_t ->
          Sigs.PROOFRULE.seq_t -> (Tagpairs.t * string) list
      type select_f = int -> Sigs.PROOFRULE.proof_t -> int list
      type t =
          int ->
          Sigs.PROOFRULE.proof_t ->
          (int list * Sigs.PROOFRULE.proof_t) Blist.t
      val mk_axiom : Sigs.PROOFRULE.axiom_f -> Sigs.PROOFRULE.t
      val mk_infrule : Sigs.PROOFRULE.infrule_f -> Sigs.PROOFRULE.t
      val mk_backrule :
        bool ->
        Sigs.PROOFRULE.select_f ->
        Sigs.PROOFRULE.backrule_f -> Sigs.PROOFRULE.t
      val all_nodes : Sigs.PROOFRULE.select_f
      val closed_nodes : Sigs.PROOFRULE.select_f
      val ancestor_nodes : Sigs.PROOFRULE.select_f
      val syntactically_equal_nodes : Sigs.PROOFRULE.select_f
      val fail : Sigs.PROOFRULE.t
      val identity : Sigs.PROOFRULE.t
      val attempt : Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
      val compose : Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
      val compose_pairwise :
        Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
      val choice : Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
      val first : Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
      val sequence : Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
      val conditional :
        (Sigs.PROOFRULE.seq_t -> bool) ->
        Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
      val combine_axioms :
        Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
    end
  module type ABDRULE =
    sig
      type seq_t
      type proof_t
      type defs_t
      type rule_t
      type select_f = int -> Sigs.ABDRULE.proof_t -> int list
      type infrule_app =
          (Sigs.ABDRULE.seq_t * Tagpairs.t * Tagpairs.t) list * string
      type abdinfrule_f =
          Sigs.ABDRULE.seq_t ->
          Sigs.ABDRULE.defs_t -> Sigs.ABDRULE.defs_t list
      type abdbackrule_f =
          Sigs.ABDRULE.seq_t ->
          Sigs.ABDRULE.seq_t ->
          Sigs.ABDRULE.defs_t -> Sigs.ABDRULE.defs_t list
      type abdgenrule_f =
          Sigs.ABDRULE.seq_t ->
          Sigs.ABDRULE.defs_t ->
          (Sigs.ABDRULE.infrule_app * Sigs.ABDRULE.defs_t) list
      type t =
          int ->
          Sigs.ABDRULE.proof_t ->
          Sigs.ABDRULE.defs_t ->
          ((int list * Sigs.ABDRULE.proof_t) * Sigs.ABDRULE.defs_t) Blist.t
      val mk_abdinfrule : Sigs.ABDRULE.abdinfrule_f -> Sigs.ABDRULE.t
      val mk_abdbackrule :
        Sigs.ABDRULE.select_f -> Sigs.ABDRULE.abdbackrule_f -> Sigs.ABDRULE.t
      val mk_abdgenrule : Sigs.ABDRULE.abdgenrule_f -> Sigs.ABDRULE.t
      val fail : Sigs.ABDRULE.t
      val lift : Sigs.ABDRULE.rule_t -> Sigs.ABDRULE.t
      val compose : Sigs.ABDRULE.t -> Sigs.ABDRULE.t -> Sigs.ABDRULE.t
      val choice : Sigs.ABDRULE.t list -> Sigs.ABDRULE.t
      val attempt : Sigs.ABDRULE.t -> Sigs.ABDRULE.t
      val first : Sigs.ABDRULE.t list -> Sigs.ABDRULE.t
    end
  module type PROVER =
    sig
      type rule_t
      module Seq : SEQUENT
      module Proof : PROOF
      val last_search_depth : int Pervasives.ref
      val idfs :
        int ->
        int ->
        Sigs.PROVER.rule_t -> Sigs.PROVER.rule_t -> Seq.t -> Proof.t option
      val print_proof_stats : Proof.t -> unit
      val melt_proof : Pervasives.out_channel -> Proof.t -> unit
    end
  module type ABDUCER =
    sig
      type abdrule_t
      type proof_t
      type defs_t
      module Seq : SEQUENT
      module Proof : PROOF
      val bfs :
        int ->
        Sigs.ABDUCER.abdrule_t ->
        Seq.t ->
        Sigs.ABDUCER.defs_t ->
        (Sigs.ABDUCER.defs_t -> bool) ->
        (Sigs.ABDUCER.proof_t * Sigs.ABDUCER.defs_t) option
      val print_proof_stats : Proof.t -> unit
      val melt_proof : Pervasives.out_channel -> Proof.t -> unit
    end
end