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 operat...