Hi People in the TPTP World,
A while back I sent out an email to people who I know are interested in non-classical logic, announcing the work that has been done to build a framework for supporting non-classical logic in the TPTP World. All the feedback we have had has been positive, and only one small change has been made (to the syntax of the long form of non-classical connectives). I'm now pleased to open the discussion to the whole TPTP World community. Here's the original message ...
Over the last couple of months we have been building the framework for
supporting non-classical logics in the TPTP World. We now have enough
developed to do end-to-end processing of normal modal logic (generic,
alethic, deontic, and epistemic) problems ... from writing the problems
in the new syntax through to finding proofs using Leo-III.
The framework we have designed is capable of much much more than normal
modal logics, but we are limiting ourselves at first so we can can get
feedback and refine our efforts. Everything is explained at ...
If you have suggestions, questions, contributions, etc., please do not
email us :-) ... we'd love to hear from you in the TPTP World Google
... where there is a conversation already started. (OK, we'll revert to
email for individual conversations.)
Geoff, Tobias (Gleissner), Alex (Steen), Chris (Benzmueller)
As before, feedback is welcome!