Logic embedding tool v1.8.4

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.

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

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 $box and $necessary).

Logic embedding tool v1.7.15

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.

We refer to 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.15 since last release:

• Added a first-order modal logic embedding that translates directly into many-sorted first-order logic (TFF). This is the default of $modal if the input is first-order (TFF). Can be overridden by parameter -p FORCE_HIGHERORDER.
• Added a new embedding for modal logic that supports non-rigid constant/function symbols. The old embedding is still available via $$modal_old.
• Contribution by @ColinRothgang: Various fixes for the embedding of dependent HOL (DOL)
• Contribution by @melanie-taprogge: Implementation of Modal-to-HOL embeddings for meta-axioms incl. interaction schemes.
• Various bug fixes and improvements

Logic embedding tool v1.7.6

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

We refer to 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.

Version 1.7.6 updates:

• Updated scala-tptp-parser to accept updated non-classical TPTP format
• Included $doxastic_modal as a mnemonic for general modal logics with more user-friendly operator names
• Contribution by @ColinRothgang: Embedding of dependent HOL into HOL (experimental)
• Modal logic embedding now supports the native equality "=" symbol
• Added support for embedding a normative domain-specific language (DSL)
• Various bug fixes and improvements

Logic embedding tool 1.7

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

We refer to the TPTP non-classical logic extension at http://tptp.org/NonClassicalLogic/ for a description of the logic specification format and the problem syntax. Currently, only modal logics are supported. More logics will be added soon.

Version 1.7 includes new supported logics: Public annoucement logics, hybrid logics and two dyadic deontic logics. See the README for details.

Logic embedding tool 1.6

embedproblem 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 THF.

We refer to the TPTP non-classical logic extension at http://tptp.org/NonClassicalLogic/ for a description of the logic specification format and the problem syntax. Currently, only modal logics are supported. More logics will be added soon.

Version 1.6 includes various bug fixes and the new sub-role syntax (see http://tptp.org/NonClassicalLogic/)

Logic embedding tool 1.5

embedproblem 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 THF.

We refer to the TPTP non-classical logic extension at http://tptp.org/NonClassicalLogic/ for a description of the logic specification format and the problem syntax.

Currently, only modal logics are supported. More logics will be added soon.