TPTP will have the following 8 operators builtin ...
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
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.
%----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 ] ] )).