The Non-classical Logics

The TPTP recognizes several normal modal logics, and one temporal logic. Each logic has a define name: Connectives
The non-classical connectives of NTF have the form {$name}. For the logics recognized by the TPTP the connectives are: (System names may also be used for user-defined connectives, e.g., {$$canadian_conditional}, thus allowing use of the TPTP syntax when experimenting with logics that have not yet been formalized in the TPTP.) A connective can be parameterized to reflect more complex non-classical connectives. The form is {$name(param1,param2,param2)}. If the connective is indexed the index is given as the first parameter prefixed with a #, e.g., {$knows(#manuel)} @ (nothing)}, so that the connective is {$knows(#manuel)} (and not the connective {$knows} applied to the index #manuel). All other parameters are key-value assignments, e.g., to list the agents of common knowledge the form might be {$common($agents:=[alice,bob,claire])}.

In NXF the non-classical connectives are applied in a mixed higher-order-applied/first-order-functional style, with the connectives applied using @ to a ()ed list of arguments. In NHF the non-classical connectives are applied using @ in usual higher-order style with curried function applications. There are also short form unary connectives for unparameterised {$box} and {$dia}, applied directly like negation: [.] and <.>, e.g., {$box} @ (p) can be written [.] p. Short forms and long forms can be used together, e.g., it’s OK to use {$necessary} and [.] in the same problem or formula.

Full specification of the connectives and their use in formulae is in the BNF starting at <nxf_atom> and <thf_defined_atomic>.

Semantics Specification
An annotated formula with the role logic is used to specify the semantics of formulae. The semantic specification typically comes first in a file. A semantic specification consists of the defined name of the logic followed by == and a list of properties value assignments. Each specification is the property name, followed by == and either a value or a tuple of specification details. If the first element of a list of details is a value, that is the default value for all cases that are not specified in the rest of the list. Each detail after the optional default value is the name of a relevant part of the vocabulary of the problem, followed by == and a value for that named part. The BNF grammar is here. The grammar is not very restrictive on purpose, to enable working with other logics as well. It is possible to create a lot of nonsense specifications, and to say the same thing in different meaningful ways. A tool to check the sanity of a specification is available.

A semantic specification changes the meaning of things such as the boolean type $o, universal quantification with !, etc - their existing meaning in classical logic should not be confused with the meaning in the declared logic.

For plain $modal and all the *_modal logics the properties that may be specified are $domains, $designation, $terms, and $modalities.

For $temporal_instant the properties are the $domains, $designation, and $terms of the modal logic, $modalities with different possible values, and another property $time.

The formulae of a problem can be either local (true in the current world) or global (true in all worlds). By default, formulae with the roles hypothesis and conjecture are local, and all others are global. These defaults can be overridden by adding a subrole, e.g., axiom-$local, conjecture-$global.