%----SIMPLE CASE
%----Standard S5 version 1
% Example problem with "standard" semantics: TODO
thf(simple_s5,logic,(
    $modal ==
      [ $constants == $rigid,
        $quantification == $constant,
        $modalities == $modal_system_S5 ] )).

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


%----CONSTANTS OPTIONS
% Example problem with at least one flexible constant: TODO
% Example problem with at least one flexible and rigid constant: TODO

%----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,
        $modalities == $modal_system_S5 ] )).


%----QUANTIFICATION OPTIONS
% Example problem with at least one constant domain: TODO
% Example problem with at least one cumulative domain: PUZ149*.p
% Example problem with at least one varying domain: PUZ087*.p
% Example problem with at least two different types of domains: TODO

%----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 ],
        $modalities == $modal_system_S5 ] )).


%----CONSEQUENCE OPTIONS
% Example problem with at least one local axiom: TODO
% Example problem with at least one global axiom: TODO
% Example problem with at least one local and one global axiom: TODO
% Example problem with local conjecture: TODO
% Example problem with global conjecture: TODO

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

thf(different_consequence,logic,(
    $modal ==
      [ $constants == $rigid,
        $quantification == $constant,
        $modalities == $modal_system_S5 ] )).


%----MODALITY OPTIONS
% Example problem with at least two different modalities: TODO

%----Special semantics for modalities with index a and b (here: systems KB and 
%----K); one default value for all other modalities (here: system S5)
thf(exotic,logic,(
    $modal ==
      [ $constants == $flexible,
        $quantification == $cumulative,
        $modalities ==
          [ $modal_system_S5,
            [#a] == $modal_system_KB,
            [#b] == $modal_system_K ] ] )).

thf(exotic,logic,(
    $modal ==
      [ $constants == $flexible,
        $quantification == $cumulative,
        $modalities ==
          [ $modal_system_S5,
            {$necessary(#a)} == $modal_system_KB,
            {$necessary(#b)} == $modal_system_K ] ] )).