1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
% COMMAND-LINE: --finite-model-find
% EXPECT: % SZS status CounterSatisfiable for SYO056^1
%------------------------------------------------------------------------------
% File : SYO056^1 : TPTP v7.2.0. Released v4.0.0.
% Domain : Logic Calculi (Quantified multimodal logic)
% Problem : Simple textbook example 13
% Version : [Ben09] axioms.
% English :
% Refs : [Gol92] Goldblatt (1992), Logics of Time and Computation
% : [Ben09] Benzmueller (2009), Email to Geoff Sutcliffe
% Source : [Ben09]
% Names : ex13.p [Ben09]
% Status : CounterSatisfiable
% Rating : 0.25 v7.2.0, 0.33 v6.4.0, 0.00 v6.3.0, 0.33 v5.4.0, 0.00 v5.0.0, 0.67 v4.1.0, 0.50 v4.0.0
% Syntax : Number of formulae : 64 ( 0 unit; 32 type; 31 defn)
% Number of atoms : 238 ( 36 equality; 137 variable)
% Maximal formula depth : 12 ( 6 average)
% Number of connectives : 138 ( 4 ~; 4 |; 8 &; 114 @)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% ( 0 ~|; 0 ~&)
% Number of type conns : 172 ( 172 >; 0 *; 0 +; 0 <<)
% Number of symbols : 36 ( 32 :; 0 =)
% Number of variables : 87 ( 3 sgn; 30 !; 6 ?; 51 ^)
% ( 87 :; 0 !>; 0 ?*)
% ( 0 @-; 0 @+)
% SPC : TH0_CSA_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
%----Include embedding of quantified multimodal logic in simple type theory
%% include('Axioms/LCL013^0.ax').
%------------------------------------------------------------------------------
thf(mvalid_type,type,(
mvalid: ( $i > $o ) > $o )).
thf(mvalid,definition,
( mvalid
= ( ^ [Phi: $i > $o] :
! [W: $i] :
( Phi @ W ) ) )).
thf(mforall_prop_type,type,(
mforall_prop: ( ( $i > $o ) > $i > $o ) > $i > $o )).
thf(mforall_prop,definition,
( mforall_prop
= ( ^ [Phi: ( $i > $o ) > $i > $o,W: $i] :
! [P: $i > $o] :
( Phi @ P @ W ) ) )).
thf(mnot_type,type,(
mnot: ( $i > $o ) > $i > $o )).
thf(mnot,definition,
( mnot
= ( ^ [Phi: $i > $o,W: $i] :
~ ( Phi @ W ) ) )).
thf(mor_type,type,(
mor: ( $i > $o ) > ( $i > $o ) > $i > $o )).
thf(mor,definition,
( mor
= ( ^ [Phi: $i > $o,Psi: $i > $o,W: $i] :
( ( Phi @ W )
| ( Psi @ W ) ) ) )).
thf(mimplies_type,type,(
mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o )).
thf(mimplies,definition,
( mimplies
= ( ^ [Phi: $i > $o,Psi: $i > $o] :
( mor @ ( mnot @ Phi ) @ Psi ) ) )).
thf(mbox_type,type,(
mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o )).
thf(mbox,definition,
( mbox
= ( ^ [R: $i > $i > $o,Phi: $i > $o,W: $i] :
! [V: $i] :
( ~ ( R @ W @ V )
| ( Phi @ V ) ) ) )).
thf(conj,conjecture,(
! [R: $i > $i > $o] :
( mvalid
@ ( mforall_prop
@ ^ [A: $i > $o] :
( mforall_prop
@ ^ [B: $i > $o] :
( mimplies @ ( mbox @ R @ ( mor @ A @ B ) ) @ ( mor @ ( mbox @ R @ A ) @ ( mbox @ R @ B ) ) ) ) ) ) )).
%------------------------------------------------------------------------------
|
