logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Builtin

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 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