Logic embedding tool v1.7.16
The logic embedding tool is a tool for embedding non-classical logics into higher-order logic (HOL). The tool translates a TPTP problem statement formulated in a non-classical logic (using the logic specification format) into monomorphic or polymorphic TPTP 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.7.16 since last release:
- README improvements
- Updated modal logic embeddings and hybrid logic embeddings to the new parameter names (as used in papers, see README).
- Aligned first-order and higher-order modal logic embedding in terms of supported operator names (such as
$boxand$necessary).