#### logtk 2.1 2.0 1.6 1.5.1 0.8.1

Core types and algorithms for logic
IN THIS PACKAGE
Module .

## Builtin Objects

Most objects that have a special meaning in logic are represented by a builtin. A builtin is a value of type `t`; it might correspond to different names in different input syntaxes.

Builtins cover numbers, connectives, and builtin types, among others.

• since 1.5
`val _t_bigger_false : bool ref`
`type t = `
 `| Not` `| And` `| Or` `| Imply` `| Equiv` `| Xor` `| Eq` `| Neq` `| HasType` `| True` `| False` `| Arrow` `| Wildcard` `| Multiset` `| TType` `| Prop` `| Term` `| ForallConst` (*constant for simulating forall*) `| ExistsConst` (*constant for simulating exists*) `| ChoiceConst` `| Grounding` (*used for inst-gen*) `| TyInt` `| TyRat` `| TyReal` `| Int of Logtk_arith.Z.t` `| Rat of Logtk_arith.Q.t` `| Real of string` `| Floor` `| Ceiling` `| Truncate` `| Round` `| Prec` `| Succ` `| Sum` `| Difference` `| Uminus` `| Product` `| Quotient` `| Quotient_e` `| Quotient_t` `| Quotient_f` `| Remainder_e` `| Remainder_t` `| Remainder_f` `| Is_int` `| Is_rat` `| To_int` `| To_rat` `| Less` `| Lesseq` `| Greater` `| Greatereq` `| Box_opaque` (*hint not to open this formula*) `| Pseudo_de_bruijn of int` (*magic to embed De Bruijn indices in normal terms*) `| BComb` (*BCIKS combinators*) `| CComb` `| IComb` `| KComb` `| SComb` `| Distinct`
`include Interfaces.HASH with type t := t`
`include Interfaces.EQ with type t := t`
`include Interfaces.ORD with type t := t`
`include Interfaces.PRINT with type t := t`
`type fixity = `
 `| Infix_binary` `| Infix_nary` `| Prefix`
`val fixity : t -> fixity`
`val is_prefix : t -> bool`

`is_infix s` returns `true` if the way the symbol is printed should be used in a prefix way if applied to 1 argument

`val is_infix : t -> bool`

`is_infix s` returns `true` if the way the symbol is printed should be used in an infix way if applied to two arguments

`val ty : t -> [ `Int | `Rat | `Other ]`
`val mk_int : Logtk_arith.Z.t -> t`
`val of_int : int -> t`
`val int_of_string : string -> t`
`val mk_rat : Logtk_arith.Q.t -> t`
`val of_rat : int -> int -> t`
`val rat_of_string : string -> t`
`val is_int : t -> bool`
`val is_rat : t -> bool`
`val is_numeric : t -> bool`
`val is_not_numeric : t -> bool`
`val is_arith : t -> bool`

Any arithmetic operator, or constant

`val is_logical_op : t -> bool`

Any arithmetic operator, or constant

`val is_logical_binop : t -> bool`
`val is_flattened_logical : t -> bool`
`val is_quantifier : t -> bool`
`val is_combinator : t -> bool`
`val true_ : t`
`val false_ : t`
`val eq : t`
`val neq : t`
`val imply : t`
`val equiv : t`
`val xor : t`
`val not_ : t`
`val and_ : t`
`val or_ : t`
`val arrow : t`
`val tType : t`
`val prop : t`
`val term : t`
`val ty_int : t`
`val ty_rat : t`
`val ty_real : t`
`val has_type : t`
`val wildcard : t`

\$_ for type inference

`val multiset : t`

type of multisets

`val grounding : t`
`val as_int : t -> int`
`module Arith : sig ... end`
`include Interfaces.HASH with type t := t`
`include Interfaces.EQ with type t := t`
`val equal : t -> t -> bool`
`val hash : t -> int`
`include Interfaces.ORD with type t := t`
`val compare : t -> t -> int`
`include Interfaces.PRINT with type t := t`
`val pp : t CCFormat.printer`
`val to_string : t -> string`
`module Map : Iter.Map.S with type key = t`
`module Set : Iter.Set.S with type elt = t`
`module Tbl : Hashtbl.S with type key = t`
`module Tag : sig ... end`

Each tag describes an extension of FO logic

### TPTP Interface

Creates symbol and give them properties.

`module TPTP : sig ... end`

The module `ArithOp` deals only with numeric constants, i.e., all symbols must verify `is_numeric` (and most of the time, have the same type). The semantics of operations follows TPTP.

`module ArithOp : sig ... end`

### ZF

`module ZF : sig ... end`