Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Mainly used to parse first-order terms, it is also used to parse tptp's THF language, which uses higher order terms, so some first-order constructs such as conjunction, equality, etc... also need to be represented by standalone terms.

Signature required by terms for typing first-order polymorphic terms.

Minimum required to type dimacs

Minimum required to type ae's tff

Minimum required to type ae's arith

Minimum required to type ae's bitvectors

Minimum required to type tptp's tff

Minimum required to type tptp's thf

Common signature for tptp arithmetics

Signature required by terms for typing tptp arithmetic.

Minimum required to type smtlib's core theory.

Common signature for first-order arithmetic

Signature required by terms for typing smtlib int arithmetic.

Signature required by terms for typing smtlib real arithmetic.

Signature required by terms for typing smtlib real_int arithmetic.

Bitvector part of the smtlib float requirements

Real part of the smtlib float requirements

Float part of the smtlib float requirements

Floating points are complicated so this documentation is not in anyway sufficient. A detailed description of the theory together with the rationale of several models decisions as well as a formal semantics of the theory can be found in