package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
type t =
  1. | Not
  2. | And
  3. | Or
  4. | Imply
  5. | Equiv
  6. | Xor
  7. | Eq
  8. | Neq
  9. | HasType
  10. | True
  11. | False
  12. | Arrow
  13. | Wildcard
  14. | Multiset
  15. | TType
  16. | Prop
  17. | Term
  18. | ForallConst
    (*

    constant for simulating forall

    *)
  19. | ExistsConst
    (*

    constant for simulating exists

    *)
  20. | Grounding
    (*

    used for inst-gen

    *)
  21. | TyInt
  22. | TyRat
  23. | TyReal
  24. | Int of Z.t
  25. | Rat of Q.t
  26. | Real of string
  27. | Floor
  28. | Ceiling
  29. | Truncate
  30. | Round
  31. | Prec
  32. | Succ
  33. | Sum
  34. | Difference
  35. | Uminus
  36. | Product
  37. | Quotient
  38. | Quotient_e
  39. | Quotient_t
  40. | Quotient_f
  41. | Remainder_e
  42. | Remainder_t
  43. | Remainder_f
  44. | Is_int
  45. | Is_rat
  46. | To_int
  47. | To_rat
  48. | Less
  49. | Lesseq
  50. | Greater
  51. | Greatereq
  52. | Box_opaque
    (*

    hint not to open this formula

    *)
  53. | Pseudo_de_bruijn of int
    (*

    magic to embed De Bruijn indices in normal terms

    *)
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 =
  1. | Infix_binary
  2. | Infix_nary
  3. | 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 : Z.t -> t
val of_int : int -> t
val int_of_string : string -> t
val mk_rat : 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_quantifier : 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 has_type : t
val wildcard : t

$_ for type inference

val multiset : t

type of multisets

val grounding : t
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 : Stdlib.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
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