libzipperposition

Library for Zipperposition
IN THIS PACKAGE

Main saturation algorithm.

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

module type S = sig ... end
module Make (E : Env.S) : S with module Env = E