Skip to content

Logic embedding tool v1.7.6

Compare
Choose a tag to compare
@lex-lex lex-lex released this 31 Jul 12:51
· 112 commits to master since this release

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