The TPTP Logic Specification Format

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


Motivation

Modal logics - Christoph to write up.

TPTP will have the following 8 operators builtin ...

... as if defined by ...
    thf(box_P_type,type,(
        $box_P: !>[T: $tType] : ( T > $o > $o ) )).

    thf(box_i_type,definition,(
        $box_i = ( $box_P @ $i ) )).

    thf(box_int_type,definition,(
        $box_int = ( $box_P @ $int ) )).

    thf(box_type,definition,(
        $box = ( $box_int @ 0 ) )).
... so a user could write ...
    thf(pigs_might_fly_type,type,(
        pigs_might_fly: $o )).

    thf(no_flying_pigs,axiom,(
        ~ ( $box @ pigs_might_fly ) )).

    thf(an_individual_type,type,(
        me: $i )).

    thf(i_believe,axiom,(
        $dia_i @ me @ pigs_might_fly )).

    thf(the_27_says_no_flying_pigs,axiom,(
        ~ ( $box_int @ 27 @ pigs_might_fly ) )).

    thf(agent_type,type,(
        agent: $tType )).

    thf(archer_agent,type,(
        archer: agent )).

    thf(archer_says_no_flying_pigs,axiom,(
        ~ ( $box_P @ agent @ archer @ pigs_might_fly ) )).

    thf(box_agent_defn,definition,(
        box_agent = ( $box_P @ agent ) )).

    thf(archer_still_says_no_flying_pigs,axiom,(
        ~ ( box_agent @ archer @ pigs_might_fly ) )).

Other logics

Theories - Geoff to write up


Format for Semantics Specification

Annotated formulae with the (new) role logic are used to specify the semantics of the modal logic. Such a formula begins with the keyword for the logic, which in this case is $modal, followed by := and a list of properties value assignments. Properties may be specified for $constants, $quantification, $consequence, and $modalities. Each specification is the property name, followed by := and either a value (see below for possible values) or a list 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 used for the problem (e.g., the name of a type, a symbol, an axiom, etc.) and followed by := and a specification for that named part. There may be more than one annotated formula providing the logic specification, but no item's properties may be specified more than once. As with the TPTP type system, all symbols must be defined before their semantic properties are specified.

The semantic properties and their possible values are:

The BNF grammar for this is linked from here, with the following being the semantic rules ...

<logic_defn_rule>      :== <logic_defn_LHS> <assignment> <logic_defn_RHS>
<logic_defn_LHS>       :== <logic_defn_value> | <thf_top_level_type>  | <name>
<logic_defn_LHS>       :== $constants | $quantification | $consequence |
                           $modalities
%----The $constants, $quantification, and $consequence apply to all of the
%----$modalities. Each of these may be specified only once, but not necessarily
%----all in a single annotated formula.
<logic_defn_RHS>       :== <logic_defn_value> | <thf_unitary_formula>
<logic_defn_value>     :== <defined_constant>
<logic_defn_value>     :== $rigid | $flexible |
                           $constant | $varying | $cumulative | $decreasing |
                           $local | $global |
                           $modal_system_K | $modal_system_T | $modal_system_D |
                           $modal_system_S4 | $modal_system_S5 |
                           $modal_axiom_K | $modal_axiom_T | $modal_axiom_B |
                           $modal_axiom_D | $modal_axiom_4 | $modal_axiom_5
... with some additions that affect <thf_unitary_formula>
<thf_pair_connective>  ::= <infix_equality> | <infix_inequality> |
                           <binary_connective> | <assignment>
<assignment>           ::= :=
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. The TPTP will provide some standard logic definitions, and some examples of possible use are provided below. We are considering implementing a tool to check the sanity of a specification. The list of keywords is not final.


Examples

%----Standard S5
thf(simple_s5,logic,(
    $modal :=
      [ $constants := $rigid,
        $quantification := $constant,
        $consequence :=
          [ $global ],
        $modalities := $modal_system_S5 ] )).

%----Standard S5 v2
thf(simple_s5_v2,logic,(
    [ $modal :=
        [ $constants := $rigid,
          $quantification := $constant,
          $consequence := $global,
          $modalities :=
            [ $modal_system_S5 ] ] ] )).

%----Default modality S5 as list of axioms K + T + 5
thf(simple_s5_v3,logic,(
    $modal :=
      [ $constants := $rigid,
        $quantification := $constant,
        $consequence := $global,
        $modalities :=
          [ $modal_axiom_K,
            $modal_axiom_T,
            $modal_axiom_5 ] ] )).

%----Constants The constant king_of_france has special semantics
thf(human_type,type,(
    human: $tType )).

thf(king_of_france_constant,type,(
    king_of_france: human )).

thf(constants,logic,(
    $modal :=
      [ $constants :=
          [ $constant,
            king_of_france := $flexible ],
        $quantification := $constant,
        $consequence := $global,
        $modalities := $modal_system_S5 ] )).

%----Quantification may be different for any base type or compound type e.g.
%----for type plushie
thf(plushie_type,type,(
    plushie: $tType )).

thf(quantification,logic,(
    $modal :=
      [ $constants := $rigid,
        $quantification :=
          [ $constant,
            plushie := $varying ],
        $consequence := $global,
        $modalities := $modal_system_S5 ] )).

%----Consequence. All axioms same consequence except for ax1 which has a
%----special consequence
thf(ax1,axiom,(
    $true )).

thf(different_consequence,logic,(
    $modal :=
      [ $constants := $rigid,
        $quantification := $constant,
        $consequence :=
          [ $global,
            ax1 := $local ],
        $modalities := $modal_system_S5 ] )).

%----Something more exotic. a, b, and c are indicies for multi-modal box or
%----diamond operators, e.g., If a is a $int, it could be used with $box_int
%----in an expression such as $box_int @ a @ p.
thf(exotic,logic,(
    $modal :=
      [ $constants := $flexible,
        $quantification := $cumulative,
        $consequence :=
          [ $global,
            ax1 := $local ],
        $modalities :=
          [ ! [X: $int] :
              ( X :=
                  [ $modal_axiom_K,
                    $modal_axiom_D ] ),
            a := $modal_system_S5,
            b := $modal_system_KB,
            c := $modal_system_K ] ] )).

thf(quantification,logic,( 
    $modal :=
      [ $constants := $rigid,
        $quantification := $constant,
        $consequence := $global,
        $modalities :=
          ! [X: $int] :
            $ite($greater @ X @ 0,$modal_system_K,$modal_system_KB)] )).

thf(instantiated_modality,logic,(
    $modal :=
      [ $constants := $rigid,
        $quantification := $constant,
        $consequence := $global,
        $modalities :=
          [ $modal_axiom_K,
             ( $box_P @ agent @ archer ) := $modal_system_D ] ] )).
%----If the user has specified box_agent = ( $box_P @ agent ) then the last
%----line can be simplified to (box_agent @ archer) := $modal_system_D

thf(funky_mixed,logic,(
    [ $modal :=
        [ $constants := $rigid,
          $quantification := $constant,
          $consequence := $global,
          $modalities := $modal_system_S5 ],
      $dialetheic :=
        [ $truth_values :=
            [ $true,
              $false,
              $both ],
          $embedding := $translational ] ] )).