The TPTP recognizes several normal modal logics, and one temporal logic. Each logic has a defined name:
Generic modal - $modal
Alethic modal - $alethic_modal
Deontic modal - $deontic_modal
Epistemic modal - $epistemic_modal
Doxastic modal - $doxastic_modal
Connectives
The non-classical connectives of NTF have the form {$name}. For the logics recognized by the TPTP the connectives are:
$modal - {$box}, {$dia}
$alethic_modal - {$necessary}, {$possible}
$deontic_modal - {$obligatory}, {$permissible}, {$forbidden}
$epistemic_modal - {$knows}, {$canKnow}
$doxastic_modal - {$believes}, {$canBelieve}
(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 file or formula.
Full specification of the connectives and their use in formulae is in the BNF.
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.
$domains
$constant - Constant domain semantics has all world's domains fixed the same.
$varying - Varying domain semantics has (potentially) different domains for each world.
$cumulative - Cumulative domain semantics and varying, and the domain of each world is a superset of the domains of the worlds from which it can be reached.
$decreasing - Decreasing domain semantics and varying, and the domain of each world is a subset of the domains of the worlds from which it can be reached.
$designation
$rigid - Rigid designation independent of worlds.
$flexible - Flexible designation dependent on worlds.
$terms
$local - Terms are interpreted in the local world
$global - Terms are interpreted globally in all the worlds
$modalities
A known system name in the form $modal_system_Sys
Sys ∈ { K,KB,K4,K5,K45,KB5,D,DB,D4,D5,D45,M,B,S4,S5,S5U }
A tuple of known axiom names in the form [ $modal_axiom_Ax1, $modal_axiom_Ax2, ... ]
Axi ∈ { K,M,B,D,4,5,CD,BoxM,C4,C }
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.