libzipperposition
Libzipperposition.Saturate
libzipperposition.avatar
libzipperposition.calculi
libzipperposition.induction
libzipperposition.phases
It uses inference rules and simplification rules from Superposition.
val check_timeout : float option -> bool
check whether we still have some time w.r.t timeout
type szs_status =
| Unsat of Logtk.Proof.S.t
| Sat
| Unknown
| Error of string
| Timeout
The SZS status of a state
val k_abort_after_fragment_check : bool Logtk.Flex_state.key
module type S = sig ... end
module Make (E : Env.S) : S with module Env = E