package libzipperposition

  1. Overview
  2. Docs
Library for Zipperposition

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

doc/libzipperposition.calculi/Libzipperposition_calculi/Lazy_cnf/Make/argument-1-E/C/Eligible/index.html

Module C.Eligible

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"