package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = int -> Logtk.Literal.t -> bool

Eligibility criterion for a literal

val res : clause -> t

Only literals that are eligible for resolution

val param : clause -> t

Only literals that are eligible for paramodulation

val eq : t

Equations

val filter : (Logtk.Literal.t -> bool) -> t
val max : clause -> t

Maximal literals of the clause

val pos : t

Only positive literals

val pos_eq : t

Only positive equational literals

val neg : t

Only negative literals

val always : t

All literals

val combine : t list -> t

Logical "and" of the given eligibility criteria. A literal is eligible only if all elements of the list say so.

val (**) : t -> t -> t

Logical "and"

val (++) : t -> t -> t

Logical "or"

val (~~) : t -> t

Logical "not"

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct