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 https://tptp.org/UserDocs/TPTPLanguage/TPTPLanguage.shtml#NonClassicalLogics for a description of the logic specification format and the problem syntax. See the README for supported logics.
Updates to 1.9.2 since last release:
- Writing to an output file now required the
--outputparameter on the command-line - Improved error reporting using more detailed SZS status values
- Fixed a few bugs in
$modalembedding - Fixed a bug in
$$dholembedding for dependently-typed higher-order logic (thanks to Daniel Renalter) - Fixed single quoted formulas and names in the output of the
$$dholembedding