package logtk

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

Module Logtk.BuiltinSource

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
Sourcetype 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
Sourcetype fixity =
  1. | Infix_binary
  2. | Infix_nary
  3. | Prefix
Sourceval fixity : t -> fixity
Sourceval 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

Sourceval 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

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

Any arithmetic operator, or constant

Sourceval true_ : t
Sourceval false_ : t
Sourceval eq : t
Sourceval neq : t
Sourceval imply : t
Sourceval equiv : t
Sourceval xor : t
Sourceval not_ : t
Sourceval and_ : t
Sourceval or_ : t
Sourceval arrow : t
Sourceval tType : t
Sourceval prop : t
Sourceval term : t
Sourceval ty_int : t
Sourceval ty_rat : t
Sourceval has_type : t
Sourceval wildcard : t

$_ for type inference

Sourceval multiset : t

type of multisets

Sourceval grounding : t
Sourcemodule Arith : sig ... end
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
Sourcemodule Map : Iter.Map.S with type key = t
Sourcemodule Set : Iter.Set.S with type elt = t
Sourcemodule Tbl : Hashtbl.S with type key = t
Sourcemodule Tag : sig ... end

Each tag describes an extension of FO logic

TPTP Interface

Creates symbol and give them properties.

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

Sourcemodule ArithOp : sig ... end

ZF

Sourcemodule ZF : sig ... end