Logic embedding tool v1.8.2

The logic embedding tool is a tool for embedding non-classical logics into classical logic (primarily higher-order logic (HOL), but also first-order logic in some cases). The tool translates a TPTP problem statement formulated in a non-classical logic (using the logic specification format) into monomorphic or polymorphic TPTP TFF/THF representation.

Please see the TPTP non-classical logic extension at http://tptp.org/NonClassicalLogic/ for a description of the logic specification format and the problem syntax. See the README for supported logics.

Updates to 1.8.2 since last release:

• README improvements
• Updated $modal embedding that now accepts the additional parameter $terms in the logic specification, for selection whether terms should be local or global (see README).
• $modal embedding will not automatically use first-order based embedding if the input problem is first-order modal logic, and fall back to the higher-order embedding otherwise.
• Added config files and build plugins for native image compilation