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.4 since last release:
- Fixed a bug that would omit necessary auxiliary output.