Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastructure for automated theorem proving, the TPTP World, currently supports only classical logics. This paper describes the latest extension of the TPTP World, providing languages and infrastructure for reasoning in non-classical logics. The extension integrates seamlessly with the existing TPTP World.
4 and
tool exchange, tool integration, and comparable experimental results. Originally the
TPTP World supported only first-order clause normal form (CNF) [
This paper describes the latest extension of the TPTP World, providing languages
and infrastructure for reasoning in non-classical logics [
The development of standards for ATP systems for first- and higher-order logic has traditionally focused mostly on classical logic, while many real-world applications often also require non-classical reasoning. These applications include artificial intelligence (e.g., knowledge representation, planning, multi-agent systems), philosophy (e.g., formal ethics, metaphysics), natural language semantics (e.g., generalized quantifiers, modalities), and computer science (e.g., software and hardware verification). There are also recent developments in natural and life sciences that employ logical reasoning (e.g., modelling of biochemical processes).
There has been a gradual disconnect between classical and non-classical logics in the
practical development and handling of automated reasoning technology, with classical
logics receiving greater attention. This is unfortunate because there exist ATP systems
for non-classical logics but their usage, interoperability, and incorporation within larger
contexts is hampered by their heterogeneous input formats and non-uniform modes of
result reporting. Furthermore, various non-classical logics can be reduced to classical
logics, e.g., the well-known standard translation of modal logics to classical first-order logic
[
reasoning systems. A preliminary format proposal was discussed in earlier work [
Knowledge representation formats for non-classical logics have been developed and
applied in the well known ILTP [
The “DFG syntax” [
The Knowledge Interchange Format (KIF) [
Common Logic (CL) is an ISO standard [
The OMDoc format [
Section 2 reviews the general structure of the TPTP languages and the existing TFF and THF languages, and introduces extensions to TFF and THF that underlie the new non-classical languages. Section 3 presents the new NXF and NHF languages for nonclassical logics. This includes the form of the non-classical connectives, and a format for specifying the logic to be used when reasoning. Section 5 exemplifies the new languages with multi-modal logic, including an illustrative example. Section 6 describes some tools that are being developed to process and reason in non-classical logics. Section 7 concludes. The resources being developed, including example ATP problems in modal logic, are available at https://github.com/TPTPWorld/NonClassicalLogic
The TPTP languages are human-readable, machine-parsable, flexible, and extensible
languages, suitable for writing both problems and solutions. The new TPTP languages
described in this paper support the representation of problems and solutions in
nonclassical logics2. In this section the general structure of the TPTP languages is reviewed,
and key features of the TXF and THF languages that underlie the new non-classical
languages are presented. The syntax of the TPTP languages is available in an extended
BNF [
language(name, role, formula, source, useful_info).
The languages supported are clause normal form (cnf), first-order form ( fof), typed
ifrst-order form ( tff), and typed higher-order form (thf). The name assigns a (unique)
identifier to each formula, for referring to it. The role, e.g., axiom, lemma, conjecture,
defines the use of the formula in an ATP system. In the formula, terms and atoms follow
Prolog conventions. The TPTP language also supports interpreted symbols, including:
”the type of types” $tType; types for individuals $i (ι) and booleans $o (o); types for
numbers $int (integers), $rat (rationals), and $real (reals); numeric constants such as
27, 43/92, -99.66; arithmetic predicates and functions such as $greater and $sum; the
truth constants $true and $false. The basic logical connectives are ^, !, ?, @, ~, |, &,
=>, <=, <=>, and <~>, for λ, ∀, ∃, higher-order application, ¬, ∨, ∧, ⇒, ⇐, ⇔, and ⊕
respectively. Equality and inequality are expressed as the infix operators = and !=. The
source and useful_info are optional (extra-logical) information about the origin and useful
details about the formula. See [
fof(union,axiom, ( ! [X,A,B] :
( member(X,union(A,B))
<=> ( member(X,A) | member(X,B) ) ),
file(’SET006+0.ax’,union),
[description(’Definition of union’), relevance(0.9)]).
2.2. The Existing TFF and THF Languages
The typed first-order form (TFF) language extends FOF with types and type declarations.
Predicate and function symbols can be declared before their use, with type signatures
2The development of TPTP World standards for writing ATP solutions beyond common derivations and
models is still necessary – see, e.g., [
The monomorphic variant of TFF is called TF0. For example . . .
tff(dog_decl,type, dog: $tType ). tff(human_decl,type, human: $tType ). tff(owner_of_decl,type, owner_of: dog > human ). tff(bit_decl,type, bit: (dog * human * $int) > $o ). tff(hates_decl,type, hates: (human * human) > $o ). tff(hate_the_multi_biter_dog,axiom, ! [D: dog,H: human,N: $int] :
( ( H != owner_of(D) & bit(D,H,N) & $greater(N,1) ) => hates(H,owner_of(D)) ) ).
The typed higher-order form (THF) extends TFF with higher-order notions, including the curried form of type declarations, lambda terms with a lambda binder ^ for λ, application with @, a choice binder @+ for , and a description binder @- for ι. In THF all symbols must be declared before their use (default typing is not possible).
The monomorphic variant of THF is called TH0. For example . . .
thf(dog_decl,type, dog: $tType ). thf(human_decl,type, human: $tType ). thf(owner_of_decl,type, owner_of: dog > human ). thf(owns_decl,type, owns: human > dog > $o ). thf(bit_decl,type, bit: dog > human > $int > $o ). thf(hates_decl,type, hates: human > human > $o ). thf(owns_defn,definition,
( owns = ( ^ [H: human,D: dog] : ( H = ( owner_of @ D ) ) ) ) ). 2.3. The TXF and THF Languages
The typed extended first-order form (TXF) [
tff(odie_decl,type, odie: dog ). tff(jon_decl,type, jon: human ). tff(feeds_decl,type, feeds: (human * dog) > $o ). tff(chases_decl,type, chases: (human * dog) > $o ). tff(says_decl,type, says: (human * $o) > $o ). tff(feed_the_non_biter_dog,axiom, ! [D: dog,H: human] : $ite( ? [N: $int] : ( bit(D,H,N) & $greater(N,0) ), chases(H,D), feeds(H,D)) ). tff(jon_says_a_dog_bit_him_twice,axiom, ? [D: dog] :
( D != odie & jon != owner_of(D) & says(jon,bit(D,jon,2)) ) ). tff(jon_says_truth,axiom,
! [S: $o] : ( says(jon,S) => S ) ).
In parallel to the development of TXF, THF has been revised to have the same structures
as TXF for tuples, conditional expressions, and let expressions. The revised THF provides
the basis for the non-classical typed higher-order (NHF) language described in Section 3.
In THF the features of FOOL are naturally available, and thus their presentation in
the TXF context is immediately adopted in THF. Augmenting the TH0 example from
4The language was called TFX in [
thf(odie_decl,type, thf(jon_decl,type, thf(feeds_decl,type, thf(chases_decl,type, thf(says_decl,type, odie: dog ). jon: human ). feeds: human > dog > $o ). chases: human > dog > $o ).
says: human > $o > $o ).
The non-classical typed extended first-order form (NXF) and non-classical typed higherorder form (NHF) languages are the new TPTP languages for non-classical logics, extending TXF and THF respectively (note the mnemonic ‘N’ in the names NXF and NHF, indicating Non-classical). The design of NXF and NHF adopted the following principles: (i) syntactic consistency with the underlying classical languages, (ii) a uniform syntax for a wide range of non-classical logics and connectives, and (iii) requiring minimal changes to existing parsing and reasoning software. The underlying typed languages provide users with useful expressive power, and types are necessary for some commonly needed concepts, e.g., arithmetic. Recall, however, from Section 2.2, that default typing provides an untyped first-order language too.
The new languages add new non-classical connectives (Section 3.1), and a syntax for specifying the logic to be used for reasoning (Section 4). QMLTP library problems and other sample problems have been translated to the new languages, which has provided an initial test of adequacy. Further testing with more logics is planned. 3.1. The Non-Classical Connectives NXF and NHF add a new interpreted functor-like connective form . . .
{connective_name} The connective_name is a TPTP defined symbol or system symbol, i.e., starting with $ or $$, naming a non-classical connective. If the connective_name is a TPTP defined symbol then its meaning is documented in the TPTP. If the connective_name is a system symbol then its meaning is defined by the user/ATP system being used, thus allowing the TPTP syntax to be used when experimenting with logics that have not been formalized in the TPTP. A connective_name may optionally be parameterized, as explained below. In NXF the non-classical connectives are applied in a mixed “higher-order applied”/“first-order functional” style, with the connectives applied to a ()ed list of arguments.5 In NHF he non-classical connectives are applied in higher-order style . . .
• In NXF {connective_name} @ (arg1,...,argn) is a formula, where each argi is an
NXF term. NXF terms are defined as for TXF, including formulae. • In NHF {connective_name} @ arg1 @ ... @ argn is a formula, where each argi is an
NHF term. NHF terms are defined as for THF, including formulae.
Despite their functional appearance, non-classical operators are diferent from usual predicates, as indicated by their enclosing braces. They can be supplied with an arbitrary number of both formulae and terms as arguments. The chosen format is a trade-of between conciseness and generality, and allows for a uniform representation of nonclassical operators with arbitrary arity. Augmenting the TXF and THF examples from above, using the box and diamond connectives from normal modal logic . . . tff(possible_dog_bit_owner,axiom,
{$dia} @ (? [D: dog] : bit(D,owner_of(D),1)) ). tff(jon_says_necessary_truth,axiom,
! [S: $o] : ( says(jon,S) => {$box} @ (S) ) ).
A connective_name may optionally be parameterized to reflect more complex
nonclassical connectives, e.g., in multi-modals logics where the modal operators are indexed,
in epistemic logics [
{connective_name(param1,. . . ,paramn)} If the connective is indexed, i.e., representing a family of connectives parameterized over some index set of constants, the index is given as the first argument as a constant (uninterpreted constant, number, or TPTP defined constant) prefixed with a #. All other parameters are key-value pairs of the form . . .
parameter_name := parameter_value
5This slightly unusual form was chosen to reflect pure first-order functional style, but by making the
application explicit the formulae can be parsed in Prolog - a long standing principle of the TPTP
languages [
Augmenting the unparameterised examples from above, using connectives from epistemic logic where $knows(#agent) is the knowledge operator for agent, and $common is the common knowledge operator for a set of agents encoded as a key-value parameter $agents:=[...] . . .
tff(alice_knows_its_possible_odie_bit_jon,axiom,
{$knows(#alice)} @ ({$dia} @ (bit(odie,jon,1)) ). tff(jon_says_common_knowledge,axiom, ! [S: $o] :
( says(jon,S) => {$common($agents:=[alice,bob,claire])} @ (S) ) ). thf(alice_knows_jon_owns_a_dog,axiom, {$knows(#alice)} @
? [D: dog] : ( owns @ jon @ D ) ). thf(alice_and_bob_know_jon_might_lie,axiom, ! [S: $o] :
( (says @ jon @ S ) => {$common($agents:=[alice,bob])} @ ({$dia} @ ~ S) ) ).
As was noted in Section 2.2, the default typing rules of TFF and TXF, and hence also of NXF, allows them to degenerate to untyped languages. In the following example bird and fly default to predicates of type $i > $o, tweety defaults to a constant of type $i, and X defaults to a variable of type $i. It uses an exemplary system-defined non-classical binary connective $$usually, denoting some kind of (not further specified) non-monotonic conditional: tff(birds_fly,axiom,
! [X] : {$$usually} @ (bird(X),fly(X)) ). tff(tweety_is_bird,axiom, bird(tweety) ).
tff(tweety,conjecture, fly(tweety) ).
In the world of non-classical logics the intended logic cannot always be inferred from the language used for the formulae – the same language can be used for formulae while diferent logics are used for reasoning. A paradigmatic example of this underspecification phenomenon occurs in intuitionistic logic. In modal logic, when reasoning about metaphysical necessity S5 is usually used, but when reasoning about deontic necessities a more suitable choice might be D. Thus when a formula uses a modal connective it is unknown what notion of necessity is intended, and in quantified logics it is unknown how necessity interacts with quantification, e.g., if ∀x. P (x) entails ∀x. P (x). It is therefore necessary to provide (meta-)information that specifies the logic to be used. A new kind of TPTP annotated formula has been introduced for this, with the role logic, and a “logic specification” as the formula.
A logic specification consists of a defined logic (family) name identified with a list of properties, e.g., in NXF . . .
tff(name,logic,logic_name == properties). where properties is a []ed list of key-value identities . . .
property_name == property_value where each property_name is a TPTP defined symbol or a system symbol, and each property_value is either a term of the language (often a defined constant) or a []ed list that might start with a term (often a defined constant), and otherwise contains key-value identities. If the first element of a property_value list is a term then that is the default value for all cases that are not specified by the following key-value identities. A simple example from modal logic is . . .
tff(simple_spec,logic, $modal == [ $constants == $rigid, $quantification == [ $constant, some_user_type == $varying ], $modalities == $modal_system_S5 ] ).
See Section 5 for more sophisticated examples, and Section 5.1 in particular for the explanation of the property_names and property_values used here.
The BNF grammar for logic specifications is available at the TPTP page, see footnote 3. The grammar is quite unrestrictive, and allows quite complicated specifications, e.g., arbitrary formulae can be used as property_values. It is flexible enough to be used for many diferent logics, users can create specifications for logics that are not defined in the TPTP, and it is possible to specify the same logic in diferent ways. It is also possible (users beware) to write meaningless specifications in a syntactically well-formed way – a tool to check the sanity of a specification is available (see Section 6). It is also clear that the logic specification resources provided at this stage of development should not already be considered exhaustive and conclusive; the property-value pairs currently supported arise from needs and experience with the range of logics currently under consideration, and might be further modified and extended.
A NXF or NHF problem file must have one logic specification, and it typically comes ifrst in the file. The logic specification binds meta-logical information to the object-level information in the problem formulae. It is an error to use a non-classical connective without a logic specification, or to underspecify the logic. Note that the logic specification can change the meaning of language features such as truth-values, universal quantification, etc. – existing meanings from classical logic should not be confused with the meanings in the declared logic.
Quantified normal multi-modal logics [
Quantified normal multi-modal logic is named $modal in the TPTP. The connectives are {$box} and {$dia}, with the indexed forms {$box(#i)} and {$dia(#i)}. The indices are uninterpreted constants on the meta-level, as described in Section 3.1. For increased readability, the TPTP also defines specialized modal logics with more specific names for the connectives. The logics are $alethic_modal, $deontic_modal, and $epistemic_modal. Each of the these is identical to $modal in terms of syntax and parameterization except that {$box} and {$dia} are renamed to {$necessary} and {$possible}, {$obligatory} and {$permissible}, and {$knows} and {$believes}, respectively.
Logic specifications for $modal use three semantically oriented properties that
characterize the logic to be used. The property names and their possible values are shown in
Table 1.7
• The $constants property specifies whether symbols are interpreted as $rigid,
i.e. interpreted as the same domain element in every world, or as $flexible, i.e.,
possibly interpreted as diferent domain elements in diferent worlds. The property
can provide a single value for all symbols, or a default value and individual values
for some symbols.
• The $quantification property specifies restrictions on the quantification domain
across the accessibility relation [
https://github.com/TPTPWorld/NonClassicalLogic/QMLTP
7The properties for $modal could also be characterized by proof-theoretic properties. For example,
$quantification can be characterized by properties that express whether or not the (converse) Barcan
formula is a tautology.
$cumulative, and $decreasing. The property can provide a single value for all
types, or a default value and individual values for some types.
• The $modalities property specifies properties of the connectives. Possible values are
defined for well-known modal logic systems, e.g., $modal_system_K, and individual
modal axiom schemes, e.g., $modal_axiom_5. They refer to the corresponding
systems and axiom schemes of the modal logic cube [
An example (a more sophisticated version of the example in Section 4) is ... tff(complex_spec,logic, $modal == [ $constants == [ $flexible, sun == $rigid ], $quantification == [ $constant,
planet_type == $varying], $modalities == [ $modal_system_K, {$box(#1)} == $modal_system_KB, {$box(#2)} == [ $modal_axiom_K, $modal_axiom_4 ] ] ).
In this example: • all symbols are flexible except for the symbol sun that is rigid, • quantification is over a constant domain, except for terms of type planet_type that are over varying domains, and • the default modality is K, but index #1 uses KB and index #2 uses the axiom schemes K and 4.
The TPTP provides multiple roles to distinguish between various types of formulae
that are assumed to be true at the start of reasoning, e.g., axiom, hypothesis, lemma,
etc. Following the generalized notion of consequence by Fitting and Mendelsohn [
“The number of SC members is necessarily an odd number.” The situation is formalized in NXF using logic $alethic_modal as follows (eq represents an adequately axiomatized equality predicate . . .
tff(four_members,hypothesis, eq(scMemberCount,4) ). tff(four_not_odd,hypothesis, ~ odd(4) ).
tff(agreed_rule, hypothesis, {$necessary} @ (odd(scMemberCount)) ). The discussion goes on as follows:
Tim: This rule is hopelessly inconsistent: 4 is not an odd number. It cannot possibly be! Let’s better forget about it.
Fred: I disagree, the rule per se is not inconsistent. The reason is that you take the term “the number of SC members” to rigidly denote the number 4.
Tim’s assumption that constants denote rigidly can be written in a logic specification . . . tff(tim,logic, $alethic_modal == [ $constants == $rigid, $quantification == $constant, $modalities == $modal_system_S5 ] ).
In this setting the state of afairs is indeed inconsistent as confirmed by Leo-III.
Fred continues: A better alternative is to take the term “the number of SC members” as lfexibly denoting whatever number of SC members there happen to be. So if we were, say, 3 SC members, the rule would be perfectly fine. But I agree with you that, right now, the rule is of no use for us, since we can derive a contradiction that 4 is an odd number, so anything would follow . . .
Unlike Tim, Fred reasons assumes that scMemberCount denotes flexibly. However, he also employs an (alethic) modal logic that assumes necessity implies truth, i.e., adopting the modal axiom T ( A → A) . . .
tff(fred,logic, $alethic_modal == [ $constants == [ $rigid, scMemberCount == $flexible ], $quantification == $constant, $modalities == [ $modal_axiom_K, $modal_axiom_T ] ] ).
Betty: I agree with interpreting the term “the number of SC members” flexibly as you
suggest. However, I don’t see the rule deriving a contradiction. That something needs
8They were probably proponents of the FDE logic [
Betty assumes scMemberCount denotes flexibly, while using a modal logic that does not assume the modal axiom T. For instance, this can be the modal logic D (aka. standard deontic logic – SDL, where is read normatively, e.g., as “it is obligatory that”) . . . tff(betty,logic, $alethic_modal == [ $constants == [ $rigid, scMemberCount == $flexible ], $quantification == $constant, $modalities == $modal_system_D ] ).
Nancy: Yes, I agree. The rule is perfectly consistent and, moreover, we should adopt it now! However, this means that we are actually violating the rule, so either someone else must come or one of us must go! she says, looking at Tim.
Nancy also assumes that constants denote flexibly, while employing a more sophisticated
logic, e.g., the deontic system E [
Tim: But we have to decide this by majority vote!
The TPTP problem library v9.0.0 will include modal logic problems. There is a tool
chain in place that has been used to convert QMLTP library problems to NXF and NHF,
to provide an initial set of problems. The TPTP4X utility [
A suite of tools that can read, manipulate, and reason over problems written in the
NXF and NHF languages is available in the Leo-III framework [
In order to compactly represent a set of problems using diferent logics with the same set of formulae, multiple logic specifications can be put in a problem generator file, with multiple corresponding Status values in the problem header. These will be distributed in the Generators directory of the TPTP problem library. The TPTP4X utility will expand such files to multiple individual files with a single logic specification and corresponding Status value. Selected individual files will be in the Problems directory of the TPTP.
This paper has described the new TPTP languages, NXF and NHF, for writing problems and solutions in non-classical logics. NXF and NHF support a new syntactic construct for non-classical logic connectives, and define a new type of annotated formula used to specify the logic to be used when reasoning. The use and flexibility of the proposed languages have been exemplarily demonstrated with modal logic. The proposed syntax is quite general and unrestrictive, and makes no a priori statement about semantics. Rather, the syntax provides a template that can be used with logics defined in the TPTP, and also by users who would like to have a TPTP-oriented input syntax for their specialized context. In both cases users will benefit from the TPTP infrastructure.
The SZS success and failure ontologies [
In the medium-term more non-classical logics will be standardised in the TPTP, and problems in all the defined logics will be added to the TPTP problem library. The TPTP technical manual will document the defined symbols used in these logics – the connectives and their properties, and the various components of their logic specification. As soon as an adequate number of problems and TPTP-compatible ATP systems are available for a specific non-classical logic, a division for that logic will be added to CASC [ 57]. This will foster robust ATP system development for non-classical logics. In conjunction with the technical manual, a suite of logic files that provide semi-formal machine-readable information about the non-classical logics defined in the TPTP is being developed. The logic files will contain information such as logics’ syntax, semantic, and proof-theoretic properties, etc. This is “work in progress”, which can be seen in the Logics directory of the project repository.
The TPTP syntax aims to provide a very general framework for automated reasoning in expressive formalisms, not yet addressed by this work. For example, in knowledge representation it is often necessary to flexibly combine multiple logics to capture the diferent information dimensions [ 58, 59]. Typical examples include, e.g., combinations of temporal logic with (multi-agent) epistemic logics, and deontic logic with action languages. Standard notions for systematically deriving combined logics from constituent logics in the context of normal modal logics are, among others, fusions [60] and fibrings [ 61]. In the context of the TPTP syntax, it is intriguing to consider supporting fusions or fibrings by simply providing multiple logic specifications, yielding a very expressive and flexible representation for domain-specific logics.
The first and second authors acknowledge financial support from the Luxembourg National Research Fund (FNR), under grant CORE C20/IS/14616644. The third author acknowledges financial support from the German Federal Ministry for Economic Afairs and Energy within the project “KI Wissen – Entwicklung von Methoden für die Einbindung von Wissen in maschinelles Lernen", project number 19A20020J. 8312 in Lecture Notes in Computer Science, Springer-Verlag, 2013, pp. 127–136. [55] A. Steen, logic-embedding v1.6, 2022. DOI: 10.5281/zenodo.5913216. [56] A. Steen, tptp-utils v1.1, 2021. DOI: 10.5281/zenodo.5877564. [57] G. Sutclife, The CADE ATP System Competition - CASC, AI Magazine 37 (2016) 99–101. [58] W. Carnielli, M. Coniglio, D. Gabbay, P. Gouveia, C. Sernadas, Analysis and Synthesis of Logics - How to Cut and Paste Reasoning Systems, number 35 in Applied Logic Series, Springer Verlag, 2008. [59] W. Carnielli, M. Coniglio, Combining Logics, in: E. Zalta (Ed.), Stanford Encyclopedia of Philosophy, Stanford University, 2020. [60] R. Thomason, Combinations of Tense and Modality, in: D. Gabbay, F. Guenthner (Eds.), Handbook of Philosophical Logic, volume 2, D. Reidel, 1984, pp. 135–165. [61] D. Gabbay, Fibring Logics, number 38 in Oxford Logic Guides, Clarendon Press, 1998.