dolmen

A parser library for automated deduction
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.intf
Module Dolmen_intf . Term

Signature for Parsing Logic languages

module type Logic = sig ... end

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 for Typechecked terms

module type Tff = sig ... end

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

module type Thf = sig ... end
module type Dimacs = sig ... end

Minimum required to type dimacs

module type Ae_Base = sig ... end

Minimum required to type ae's tff

module type Ae_Arith_Common = sig ... end
module type Ae_Arith = sig ... end

Minimum required to type ae's arith

module type Ae_Array = sig ... end
module type Ae_Bitv = sig ... end

Minimum required to type ae's bitvectors

module type Tptp_Tff_Core = sig ... end

Minimum required to type tptp's tff

module type Tptp_Thf_Core_Const = sig ... end
module type Tptp_Thf_Core = sig ... end

Minimum required to type tptp's thf

module type Tptp_Tff_Arith_Common = sig ... end

Common signature for tptp arithmetics

module type Tptp_Tff_Arith = sig ... end

Signature required by terms for typing tptp arithmetic.

module type Smtlib_Base = sig ... end

Minimum required to type smtlib's core theory.

module type Smtlib_Arith_Common = sig ... end

Common signature for first-order arithmetic

module type Smtlib_Int = sig ... end

Signature required by terms for typing smtlib int arithmetic.

module type Smtlib_Real = sig ... end

Signature required by terms for typing smtlib real arithmetic.

module type Smtlib_Real_Int = sig ... end

Signature required by terms for typing smtlib real_int arithmetic.

module type Smtlib_Array = sig ... end
module type Smtlib_Bitv = sig ... end
module type Smtlib_Float_Bitv = sig ... end

Bitvector part of the smtlib float requirements

module type Smtlib_Float_Real = sig ... end

Real part of the smtlib float requirements

module type Smtlib_Float_Float = sig ... end

Float part of the smtlib float requirements

module type Smtlib_Float = sig ... end

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

module type Smtlib_String_RegLan = sig ... end
module type Smtlib_String_String = sig ... end
module type Smtlib_String = sig ... end
module type Zf_Base = sig ... end
module type Zf_Arith = sig ... end