sig
  type t_logic = Classical | Intuitionistic | Minimal
  type t_options = {
    verbose : bool;
    discharge : bool;
    undischarge : bool;
    logic : Main.t_logic;
    quiet : bool;
  }
  val default_options : Main.t_options
  val conclusion_of_prf : PRF_types.t_prf -> FML_types.t_fml
  val premises_of_prf :
    FML_types.t_fml list -> PRF_types.t_prf -> FML_types.t_fml list
  val validate_prf :
    ?options:Main.t_options -> PRF_types.t_prf -> PRF_types.t_prf option
  val validate_file :
    ?options:Main.t_options -> string -> PRF_types.t_prf option
  val validate_stdin :
    ?options:Main.t_options -> unit -> PRF_types.t_prf option
  val expand_and_validate_file : ?options:Main.t_options -> string -> unit
end