# 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 ...

• \$box_P - polymorphic box (e.g., necessity), for multi-modal systems
• \$box_i - box (e.g., necessity) indexed over individuals (type \$i), for multi-modal systems
• \$box_int - box (e.g., necessity) indexed over integers (type \$int), for multi-modal systems
• \$box - box (e.g., necessity) for mono-modal systems (really \$box_int with index 0)
• \$dia_P - polymorphic diamond (e.g., possibility), for multi-modal systems
• \$dia_i - diamond (e.g., possibility) indexed over individuals (type \$i), for multi-modal systems
• \$dia_int - diamond (e.g., possibility) indexed over integers (type \$int), for multi-modal systems
• \$dia - diamond (e.g., possibility) for mono-modal systems (really \$dia_int with index 0)
... 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 ) )).
```
... and similarly for \$dia*, so a user could write ...
```    thf(pigs_might_fly_type,type,(
pigs_might_fly: \$o )).

thf(no_flying_pigs,axiom,(
~ ( \$dia @ 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,(
~ ( \$dia_int @ 27 @ pigs_might_fly ) )).

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

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

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

thf(dia_agent_defn,definition,(
dia_agent = ( \$dia_P @ agent ) )).

thf(archer_still_says_no_flying_pigs,axiom,(
~ ( dia_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:

• \$constants
• \$rigid - Rigid constants are independent of worlds.
• \$flexible - Flexible constants are dependent on worlds.
• \$quantification
• \$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.
• \$consequence
• \$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 -

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 ] ] )).
```