Non-classical Logics

by Tobias Gleißner, Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller


Extension of the TPTP TXF and THF dialects to support a wide range of non-classical logics with


The descriptions and examples below are in terms of alethic modal logic. The syntax offers much more - see the section on the exotic future below.

Connectives Long Form

Non-classical connectives belonging to a logic get unique defined names, e.g., $necessary. The connectives are written in {} brackets (to indicate that they are non-classical, and their semantics has to be defined in a semantics specification). 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. They are used in prefix form, with the arguments in ()s for TXN, and applied using @ in THN. The BNF grammar is here.


    tff(pigs_might_fly_type,type,pigs_might_fly: $o ).

        ~ ({$possible} @ (pigs_might_fly) ) ).

        ? [P: $o] : {$possible} @ (P) ).

        {$forbidden} @ pigs_might_fly ).

        ! [P: $o] : ( {$permissible} @ P ) ).
Connectives may have a list of parameters, where a parameter is one of:

Connectives Short Form

The short forms provide shorthand for the long forms. Two short forms are available in alethic modal logics: [...], <...>. The short forms are associated by TPTP standards with specific long forms in specific logics, e.g., in alethic modal logic [...] is short for {$necessary:...} and <...> is short for {$possible:...}. There might not be a short form for every long form in a given logic. The short forms may be parameterized by an index, but nothing more. A non-indexed short form has a period in the brackets. The BNF grammar is here.


        ~ (<.> @ (pigs_might_fly) ) ).

        <#me> @ (pigs_might_fly) ).

        <.> @ pigs_might_fly ).

        [#archer] @ pigs_might_fly ).
Short forms and long forms can be used together, e.g., it’s OK to use {$necessary} and [.] in the same problem or formula.

Semantics Specification

Annotated formulae with the (new) role logic are used to specify the semantics of the logic. Such a formula begins with the keyword for the logic, e.g., $modal, $alethic_modal, $deontic_modal, $epistemic_modal, 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

The semantic specification typically comes first in a problem file. A logic 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 alethic modal logics the properties that may be specified are $constants, $quantification, and $modalities. The $constants, $quantification, and $modalities may have individual values for constants and types.

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 {\tt hypothesis} and {\tt conjecture} are local, and all others are global. These defaults can be overridden by adding a subrole, e.g., {\tt axiom-\$local}, {\tt conjecture-\$global}.

See CorrectSpecifications.p for examples. 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.

TPTP Logics

Logic Name Connectives Semantics
Generic modal $modal $box, $dia $modal == [ $constants == C, $quantification == Q, $modalities == M ]
  • C ∈ { $rigid, $flexible }
  • Q ∈ { $constant, $varying, $cumulative, $decreasing }
  • M == $modal_system_Sys | [ $modal_axiom_Ax1, $modal_axiom_Ax2, ... ]
    • Sys ∈ { K,KB,K4,K5,K45,KB5,D,DB,D4,D5,D45,T,B,S4,S5,S5U }
    • Ax ∈ { K,T,B,D,4,5,CD,BoxM,C4,C }
Alethic modal $alethic_modal $necessary, $possible $alethic_modal == as for $modal
Deontic modal $deontic_modal $obligatory, $permissible, $forbidden $deontic_modal == as for $modal
Epistemic modal $epistemic_modal $knows, $canKnow $epistemic_modal == as for $modal
Doxastic modal $doxastic_modal $believes, $canBelieve $doxastic_modal == as for $modal
Temporal (instant-based) $temporal_instant $future, $past, $henceforth, $hitherto $temporal_instance == [ $constants == C, $quantification == Q, $modalities == M, $time == T ]
  • C and Q as for $modal
  • M == [ $modal_axiom_AxTm1, $modal_axiom_AxTm2, ... ]
    • Ax ∈ { K,T,B,D,4,5 }
    • Tm ∈ { +,- }
  • T ∈ { $reflexivity, $irreflexivity, $transitivity, $asymmetry, $anti_symmetry, $linearity, $forward_linearity, $backward_linearity, $beginning, $end, $no_beginning, $no_end, $density, $forward_discreteness, $backward_discreteness }


These examples can be run in Leo-III within
SystemOnTPTP. Leo-III embeds non-classical logic problems into plain THF, and solves the THF problem. The embedding tool is available as Logic2THF in SystemB4TPTP, the output from which can be given to any THF system.

Logic Documentation

The various logics, the syntax used, the axiom schemes, and the semantics specification, are being semi-formally documented in a machine readable form. This work is available in the Logics directory of the Github repository.

Exotic Future

The use of the TPTP framework for non-classical logics, as presented so far, is conservative, adopting only widely accepted structures in alethic modal logics. The TPTP framework is capable of much more. Some of our ideas are listed here, some relevant and unpolished files are in the
ExoticFuture directory, and feedback is welcome.