Non-classical Logics

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


Motivation

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

Overview

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

Connectives belonging to a logic get unique defined names, e.g., $necessary. The connective is written in {} brackets, and the application is functional. The BNF grammar is here.

Examples:

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

    tff(no_flying_pigs,axiom,
        ~ {$possible}(pigs_might_fly) ).

    tff(something_is_possible,axiom,
        ? [P: $o] : {$possible}(P) ).

    thf(forbidden_flying_pigs,axiom,
        {$forbidden} @ pigs_might_fly ).

    thf(everything_is_permissible,axiom,
        ! [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.

Examples:

    tff(no_flying_pigs,axiom,
        ~ <.>(pigs_might_fly) ).

    tff(for_me_it_is_possible,axiom,
        <#me>(pigs_might_fly) ).

    thf(forbidden_flying_pigs,axiom,
        <.> @ pigs_might_fly ).

    thf(archer_knows_flying_pigs,axiom,
        [#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 here.

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, $consequence, and $modalities. The $constants, $quantification, and $modalities may have individual values for constants and types, and the $consequence may have individual values for named axioms.

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.


Examples

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.