Module Solver.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer
module Quip : sig ... end