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