API Reference behold v#1.1.3

Provides an overview over the included functionality in this package.

Contains macros for the connectives of classical higher-order logic. This includes constants and terms facilitating pattern matching and term construction. Note that more types, constants and terms can be introduced via the HOL library.

Provides various terms constructors as macros for different notions of equality. This includes variants of Leibniz equality, Andrews equality and extensional equality.

Defines patterns on terms with respect to the definitions introduced in BeHOLd.ClassicalHOL.Definitions. Note that this should only be used for pattern matching and not for term construction!

A data structure to declare and track variable types and declared constants. Also contains type constraints needed for parsing.

A data structure to describe a (TPTP) proof problem.

Contains functionality to parse a formula in TH0 syntax with full type inference. The algorithm is similar to Hindley-Milner type systems but for simplicity reasons without the optimizations found in algorithms J or W. The type unification algorithm is documented in BeHOLd.Util.TypeInference). A context can be specified to clear up unknown types. If terms still have unknown type after parsing, unifies their type with type o. The main entry point is the parse/2 function.

Contains utility to parse files from the TPTP problem library (https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax. Also contains utility to generate TH0 string representation of terms, types and declarations. This module only works with files in TH0 syntax. For reference, the TH0 language is defined in https://doi.org/10.1007/s10817-017-9407-7.

Contains a tokenize/1 function for tokenizing a string representing a formula in TH0 syntax or a TPTP TH0 problem file using NimbleParsec. This is mainly used as a preprocessing step for parsing. For information about the returned structure, see https://hexdocs.pm/nimble_parsec/NimbleParsec.html.

Contains functionality to create and check for unknown types and a type inference engine which works by unifying constraints using Robinson's unification algorithm.