TPTP Problem File: AGT028^1.p

View Solutions - Solve Problem

%------------------------------------------------------------------------------
% File     : AGT028^1 : TPTP v7.0.0. Released v5.2.0.
% Domain   : Agents
% Problem  : Five different degrees of belief - agent 4
% Version  : [Ben11] axioms.
% English  :

% Refs     : [Ben11] Benzmueller (2011), Email to Geoff Sutcliffe
%          : [Ben11] Benzmueller (2011), Combining and Automating Classical
% Source   : [Ben11]
% Names    : Ex_11_1 [Ben11]

% Status   : Theorem
% Rating   : 0.50 v7.0.0, 0.43 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v5.5.0, 0.33 v5.4.0, 0.60 v5.2.0
% Syntax   : Number of formulae    :  145 (   0 unit;  47 type;  31 defn)
%            Number of atoms       :  926 (  36 equality; 255 variable)
%            Maximal formula depth :   11 (   7 average)
%            Number of connectives :  760 (   4   ~;   4   |;   8   &; 736   @)
%                                         (   0 <=>;   8  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of type conns  :  235 ( 235   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   51 (  47   :;   0   =)
%            Number of variables   :  147 (   3 sgn;  29   !;   6   ?; 112   ^)
%                                         ( 147   :;   0  !>;   0  ?*)
%                                         (   0  @-;   0  @+)
% SPC      : TH0_THM_EQU_NAR

% Comments : 
%------------------------------------------------------------------------------
%----Include embedding of quantified multimodal logic in simple type theory
include('Axioms/LCL013^0.ax').
%------------------------------------------------------------------------------
thf(r1,type,(
    r1: $i > $i > $o )).

thf(r2,type,(
    r2: $i > $i > $o )).

thf(r3,type,(
    r3: $i > $i > $o )).

thf(r4,type,(
    r4: $i > $i > $o )).

thf(r5,type,(
    r5: $i > $i > $o )).

thf(john,type,(
    john: mu )).

thf(tom,type,(
    tom: mu )).

thf(peter,type,(
    peter: mu )).

thf(mike,type,(
    mike: mu )).

thf(good_in_maths,type,(
    good_in_maths: mu > $i > $o )).

thf(maths_teacher,type,(
    maths_teacher: mu > $i > $o )).

thf(mathematician,type,(
    mathematician: mu > $i > $o )).

thf(maths_student,type,(
    maths_student: mu > $i > $o )).

thf(good_in_physics,type,(
    good_in_physics: mu > $i > $o )).

thf(physics_student,type,(
    physics_student: mu > $i > $o )).

thf(axiom_r1,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mimplies @ ( maths_teacher @ X ) @ ( mbox @ r4 @ ( good_in_maths @ X ) ) ) ) )).

thf(axiom_r2_1,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r5 @ ( mimplies @ ( mbox @ r1 @ ( mathematician @ X ) ) @ ( mbox @ r1 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r2_2,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r5 @ ( mimplies @ ( mbox @ r2 @ ( mathematician @ X ) ) @ ( mbox @ r2 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r2_3,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r5 @ ( mimplies @ ( mbox @ r3 @ ( mathematician @ X ) ) @ ( mbox @ r3 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r2_4,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r5 @ ( mimplies @ ( mbox @ r4 @ ( mathematician @ X ) ) @ ( mbox @ r4 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r2_5,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r5 @ ( mimplies @ ( mbox @ r5 @ ( mathematician @ X ) ) @ ( mbox @ r5 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r3_1,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( maths_student @ X ) @ ( mdia @ r1 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r3_2,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( maths_student @ X ) @ ( mdia @ r2 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r3_3,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( maths_student @ X ) @ ( mdia @ r3 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r3_4,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( maths_student @ X ) @ ( mdia @ r4 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r3_5,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( maths_student @ X ) @ ( mdia @ r5 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_r4_1,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( physics_student @ X ) @ ( mdia @ r1 @ ( good_in_physics @ X ) ) ) ) ) )).

thf(axiom_r4_2,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( physics_student @ X ) @ ( mdia @ r2 @ ( good_in_physics @ X ) ) ) ) ) )).

thf(axiom_r4_3,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( physics_student @ X ) @ ( mdia @ r3 @ ( good_in_physics @ X ) ) ) ) ) )).

thf(axiom_r4_4,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( physics_student @ X ) @ ( mdia @ r4 @ ( good_in_physics @ X ) ) ) ) ) )).

thf(axiom_r4_5,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r3 @ ( mimplies @ ( physics_student @ X ) @ ( mdia @ r5 @ ( good_in_physics @ X ) ) ) ) ) )).

thf(axiom_r5,axiom,
    ( mvalid
    @ ( mforall_ind
      @ ^ [X: mu] :
          ( mbox @ r2 @ ( mimplies @ ( good_in_physics @ X ) @ ( mdia @ r2 @ ( good_in_maths @ X ) ) ) ) ) )).

thf(axiom_a6,axiom,
    ( mvalid @ ( maths_teacher @ john ) )).

thf(axiom_a7,axiom,
    ( mvalid @ ( mbox @ r2 @ ( mathematician @ tom ) ) )).

thf(axiom_a8,axiom,
    ( mvalid @ ( mbox @ r5 @ ( maths_student @ peter ) ) )).

thf(axiom_a9,axiom,
    ( mvalid @ ( mbox @ r5 @ ( physics_student @ mike ) ) )).

thf(axiom_D_for_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r1 @ Phi ) @ ( mnot @ ( mbox @ r1 @ ( mnot @ Phi ) ) ) ) ) )).

thf(axiom_D_for_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mnot @ ( mbox @ r2 @ ( mnot @ Phi ) ) ) ) ) )).

thf(axiom_D_for_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mnot @ ( mbox @ r3 @ ( mnot @ Phi ) ) ) ) ) )).

thf(axiom_D_for_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mnot @ ( mbox @ r4 @ ( mnot @ Phi ) ) ) ) ) )).

thf(axiom_D_for_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mnot @ ( mbox @ r5 @ ( mnot @ Phi ) ) ) ) ) )).

thf(axiom_I_for_r2_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mbox @ r1 @ Phi ) ) ) )).

thf(axiom_I_for_r3_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r1 @ Phi ) ) ) )).

thf(axiom_I_for_r4_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r1 @ Phi ) ) ) )).

thf(axiom_I_for_r45r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r1 @ Phi ) ) ) )).

thf(axiom_I_for_r3_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r2 @ Phi ) ) ) )).

thf(axiom_I_for_r4_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r2 @ Phi ) ) ) )).

thf(axiom_I_for_r5_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r2 @ Phi ) ) ) )).

thf(axiom_I_for_r4_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r3 @ Phi ) ) ) )).

thf(axiom_I_for_r5_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r3 @ Phi ) ) ) )).

thf(axiom_I_for_r5_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r4 @ Phi ) ) ) )).

thf(axiom_4s_for_r1_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r1 @ Phi ) @ ( mbox @ r1 @ ( mbox @ r1 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r1_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r1 @ Phi ) @ ( mbox @ r2 @ ( mbox @ r1 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r1_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r1 @ Phi ) @ ( mbox @ r3 @ ( mbox @ r1 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r1_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r1 @ Phi ) @ ( mbox @ r4 @ ( mbox @ r1 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r1_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r1 @ Phi ) @ ( mbox @ r5 @ ( mbox @ r1 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r2_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mbox @ r1 @ ( mbox @ r2 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r2_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mbox @ r2 @ ( mbox @ r2 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r2_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mbox @ r3 @ ( mbox @ r2 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r2_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mbox @ r4 @ ( mbox @ r2 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r2_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r2 @ Phi ) @ ( mbox @ r5 @ ( mbox @ r2 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r3_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r1 @ ( mbox @ r3 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r3_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r2 @ ( mbox @ r3 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r3_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r3 @ ( mbox @ r3 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r3_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r4 @ ( mbox @ r3 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r3_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r3 @ Phi ) @ ( mbox @ r5 @ ( mbox @ r3 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r4_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r1 @ ( mbox @ r4 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r4_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r2 @ ( mbox @ r4 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r4_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r3 @ ( mbox @ r4 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r4_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r4 @ ( mbox @ r4 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r4_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r4 @ Phi ) @ ( mbox @ r5 @ ( mbox @ r4 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r5_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r1 @ ( mbox @ r5 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r5_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r2 @ ( mbox @ r5 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r5_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r3 @ ( mbox @ r5 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r5_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r4 @ ( mbox @ r5 @ Phi ) ) ) ) )).

thf(axiom_4s_for_r5_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mbox @ r5 @ Phi ) @ ( mbox @ r5 @ ( mbox @ r5 @ Phi ) ) ) ) )).

thf(axiom_5_for_r1,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mnot @ ( mbox @ r1 @ Phi ) ) @ ( mbox @ r1 @ ( mnot @ ( mbox @ r1 @ Phi ) ) ) ) ) )).

thf(axiom_5_for_r2,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mnot @ ( mbox @ r2 @ Phi ) ) @ ( mbox @ r2 @ ( mnot @ ( mbox @ r2 @ Phi ) ) ) ) ) )).

thf(axiom_5_for_r3,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mnot @ ( mbox @ r3 @ Phi ) ) @ ( mbox @ r3 @ ( mnot @ ( mbox @ r3 @ Phi ) ) ) ) ) )).

thf(axiom_5_for_r4,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mnot @ ( mbox @ r4 @ Phi ) ) @ ( mbox @ r4 @ ( mnot @ ( mbox @ r4 @ Phi ) ) ) ) ) )).

thf(axiom_5_for_r5,axiom,
    ( mvalid
    @ ( mforall_prop
      @ ^ [Phi: $i > $o] :
          ( mimplies @ ( mnot @ ( mbox @ r5 @ Phi ) ) @ ( mbox @ r5 @ ( mnot @ ( mbox @ r5 @ Phi ) ) ) ) ) )).

thf(conj,conjecture,
    ( mvalid
    @ ( mexists_ind
      @ ^ [X: mu] :
          ( mbox @ r4 @ ( good_in_maths @ X ) ) ) )).

%------------------------------------------------------------------------------