-
Notifications
You must be signed in to change notification settings - Fork 72
/
tinyHOL.kif
95 lines (70 loc) · 2.88 KB
/
tinyHOL.kif
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
(domain modalAttribute 1 Formula)
(domain modalAttribute 2 NormativeAttribute)
(instance modalAttribute BinaryPredicate)
(subclass Formula Physical)
(subclass DeonticAttribute Attribute)
(instance Obligation DeonticAttribute)
(instance Permission DeonticAttribute)
(instance Prohibition DeonticAttribute)
;; Problem 1
(instance knows BinaryPredicate)
(domain knows 1 AutonomousAgent)
(domain knows 2 Formula)
(instance believes BinaryPredicate)
(domain believes 1 AutonomousAgent)
(domain believes 2 Formula)
(instance Bill Human)
(instance Joe Human)
(father Bill Joe)
(instance Jane Human)
(father Bill Jane)
(knows Bill
(and
(father Bill Joe)
(father Bill Jane)))
; (knows Bill (father Bill Joe))
; thf(conj,conjecture, (( (knows_THFTYPE_IiooI @ lBill_THFTYPE_i @
; (father_THFTYPE_IiioI @ lBill_THFTYPE_i @ lJoe_THFTYPE_i)) ))).
;; Problem 2
(modalAttribute
(exists (?BT)
(and
(instance ?BT BrushingTeeth)
(agent ?BT Joe)))
Obligation)
; THF version of above
; thf(ax49,axiom,((modalAttribute_THFTYPE_IoioI @ (? [BT: $i]:
; ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
; (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i))) @ lObligation_THFTYPE_i))).
; we have (modalAttribute P Obligation) so we should be able to conclude
; (not (modalAttribute (not P) Permission)) and also
; (modalAttribute P Permission)
;------------------------------------------
; SUMO query 1
; (modalAttribute (exists (?BT) (and (instance ?BT BrushingTeeth)
; (agent ?BT Joe))) Permission))
; THF query 1
; thf(conj,conjecture,((modalAttribute_THFTYPE_IoioI @ ((? [BT: $i]:
; ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
; (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i)))) @ lPermission_THFTYPE_i))).
; linear for pasting -
; thf(conj,conjecture,((modalAttribute_THFTYPE_IoioI @ ((? [BT: $i]: ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) & (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i)))) @ lPermission_THFTYPE_i))).
; no proof - don't know why
; it should follow that from
; thf(ax54,axiom,((! [FORMULA: $i]:
; ((modalAttribute_THFTYPE_IiioI @ FORMULA @ lObligation_THFTYPE_i) =>
; (modalAttribute_THFTYPE_IiioI @ FORMULA @ lPermission_THFTYPE_i))))).
; and
; thf(ax49,axiom,((modalAttribute_THFTYPE_IoioI @ (? [BT: $i]:
; ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
; (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i))) @ lObligation_THFTYPE_i))).
; thf(conj,conjecture,((modalAttribute_THFTYPE_IoioI @ (~ (? [BT: $i]:
; ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
; (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i)))) @ lProhibition_THFTYPE_i))).
; thf(conj,conjecture,(? [V: $i, P : $o] : (~ (modalAttribute_THFTYPE_IoioI @ ~P @ V)))).
(=>
(modalAttribute ?FORMULA Obligation)
(modalAttribute ?FORMULA Permission))
(=>
(modalAttribute ?F Necessity)
(modalAttribute ?F Possibility))