#### logtk 2.1 2.0 1.6 1.5.1 0.8.1

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
Module .

## Literals

Literals are the representation of atomic formulas in the clausal world of resolution/superposition provers.

A literal is an atomic formula (equality or predicate), paired with a sign that carries negation.

`type term = Term.t`
`type t = private `
 `| True` `| False` `| Equation of term * term * bool`

a literal, that is, a signed atomic formula

`val equal_com : t -> t -> bool`

commutative equality of lits

`val compare : t -> t -> int`

lexicographic comparison of literals

`include Interfaces.HASH with type t := t`
`include Interfaces.EQ with type t := t`
`val equal : t -> t -> bool`
`val hash : t -> int`

hashing of literal

`val weight : t -> int`

weight of the lit (sum of weights of terms)

`val ho_weight : t -> int`

weight of the lit (sum of weights of terms)

ho weight of the lit (sum of weights of terms, ignoring applied variables and lambda prefixes

`val heuristic_weight : ( term -> int ) -> t -> int`

ho weight of the lit (sum of weights of terms, ignoring applied variables and lambda prefixes

heuristic difficulty to eliminate lit

`val depth : t -> int`

depth of literal

`val eqn_sign : t -> bool`

equation sign: T for s=t and F for s!=t

`val is_positivoid : t -> bool`

is the literal s=t where neither s nor t are T or F or of the form s = T?

`val is_negativoid : t -> bool`

is the literal of the form s!=t or of the form s = F

`val is_eqn : t -> bool`

is the literal a proper (in)equation or prop?

`val is_prop : t -> bool`

is the literal a boolean proposition?

`val is_eq : t -> bool`

is the literal of the form a = b?

`val is_neq : t -> bool`

is the literal of the form a != b?

`val mk_eq : term -> term -> t`

build literals. If sides so not have the same sort, a SortError will be raised. An ordering must be provided

`val mk_neq : term -> term -> t`
`val mk_lit : term -> term -> bool -> t`
`val mk_prop : term -> bool -> t`

proposition

`val mk_true : term -> t`

true proposition

`val mk_false : term -> t`

false proposition

`val mk_tauto : t`

tautological literal

`val mk_absurd : t`

absurd literal, like ~ true

`val no_prop_invariant : t -> bool`
`val mk_constraint : term -> term -> t`

`mk_constraint t u` makes a disequation or a HO constraint depending on how `t` and `u` look.

```val matching : ?subst:Subst.t -> pattern:t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t```

checks whether subst(lit_a) matches lit_b. Returns alternative substitutions s such that s(lit_a) = lit_b and s contains subst.

```val subsumes : ?subst:Subst.t -> t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t```

More general version of `matching`, yields `subst` such that `subst(lit_a) => lit_b`.

`val are_opposite_subst : subst:Subst.t -> t Scoped.t -> t Scoped.t -> bool`

Literals are equal according to given substitution for variables, but are of opposite sign

`val are_opposite_same_sc : t -> t -> bool`

Literals are equal, but are of opposite signs

```val variant : ?subst:Subst.t -> t Scoped.t -> t Scoped.t -> (Subst.t * Builtin.Tag.t list) Iter.t```
```val unify : ?subst:Unif_subst.t -> t Scoped.t -> t Scoped.t -> (Unif_subst.t * Builtin.Tag.t list) Iter.t```
`val are_variant : t -> t -> bool`
`val apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t`
`val apply_subst_no_simp : Subst.Renaming.t -> Subst.t -> t Scoped.t -> t`
`val apply_subst_list : Subst.Renaming.t -> Subst.t -> t list Scoped.t -> t list`
`exception Lit_is_constraint`
`val negate : t -> t`

negate literal

`val is_constraint : t -> bool`

Is the literal a constraint?

`val is_ho_constraint : t -> bool`
`val of_unif_subst : Subst.Renaming.t -> Unif_subst.t -> t list`

Make a list of (negative) literals out of the unification constraints contained in this substitution.

`val map : ( term -> term ) -> t -> t`

functor

`val fold : ( 'a -> term -> 'a ) -> 'a -> t -> 'a`

basic fold

`val for_all : ( term -> bool ) -> t -> bool`

for the term or both terms of the literal

`val vars : t -> Type.t HVar.t list`

gather variables

`val var_occurs : Type.t HVar.t -> t -> bool`
`val is_ground : t -> bool`
`val symbols : ?include_types:bool -> t -> ID.Set.t`
`val root_terms : t -> term list`

all the terms immediatly under the lit

`val to_ho_term : t -> term option`

Conversion to higher-order term using `Term.Form`

`val as_ho_predicate : t -> (Term.var * term * term list * bool) option`

View on literals `F t1…tn` and `¬ (F t1…tn)`

`val is_ho_predicate : t -> bool`
`module Set : CCSet.S with type elt = t`

### Basic semantic checks

`val is_trivial : t -> bool`
`val is_absurd : t -> bool`
`val is_absurd_tags : t -> Proof.tag list`

if `is_absurd lit`, return why

`val is_app_var_eq : t -> bool`

if `is_absurd lit`, return why

`val is_type_pred : t -> bool`
`val is_typex_pred : t -> bool`
`val is_predicate_lit : t -> bool`
`val as_inj_def : t -> (ID.t * (Term.var * Term.var) list) option`
`val is_pure_var : t -> bool`
`val as_pos_pure_var : t -> (Term.var * Term.var) option`
`val max_term_positions : ord:Ordering.t -> t -> int`
```val fold_terms : ?position:Position.t -> ?vars:bool -> ?var_args:bool -> ?fun_bodies:bool -> ?ty_args:bool -> which:[< `Max | `All ] -> ?ord:Ordering.t -> subterms:bool -> t -> term Position.With.t Iter.t```

Iterate on terms, maybe subterms, of the literal. Variables are ignored if `vars` is `false`.

`vars` decides whether variables are iterated on too (default `false`) `var_args` decides whether arguments of applied variables are iterated on too `fun_bodies` decides whether bodies of lambda-expressions are iterated on too `ty_args` decides whether type arguments are iterated on too `subterms` decides whether strict subterms, not only terms that occur directly under the literal, are explored.

`which` is used to decide which terms to visit:

• if `which` is ``Max`, only the maximal terms are explored
• if `which` is ``All`, all root terms are explored
`val normalize_eq : t -> t option`
`module Comp : sig ... end`
`module Seq : sig ... end`
`module Pos : sig ... end`
`val replace : t -> old:term -> by:term -> t`

`replace lit ~old ~by` syntactically replaces all occurrences of `old` in `lit` by the term `by`.

`module View : sig ... end`
`module Conv : sig ... end`

### IO

`type print_hook = CCFormat.t -> t -> bool`

might print the literal on the given buffer.

• returns

true if it printed, false otherwise

`val add_default_hook : print_hook -> unit`
`val pp_debug : ?hooks:print_hook list -> t CCFormat.printer`
`val pp : t CCFormat.printer`
`val pp_zf : t CCFormat.printer`
`val pp_tstp : t CCFormat.printer`
`val to_string : t -> string`