forked from ontologyportal/sumo
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHOL.kif
114 lines (96 loc) · 2.35 KB
/
HOL.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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
;; copyright Infosys 2019
;; author - Adam Pease - [email protected]
;; Access to and use of these products is governed by the GNU General Public
;; License <http://www.gnu.org/copyleft/gpl.html>.
;; By using these products, you agree to be bound by the terms
;; of the GPL.
;; experiments in higher order logic
;; fanciful test case problem of my Mom tells me to brush my teeth
;; from SUMO - call it SUMO1
(=>
(modalAttribute ?FORMULA Obligation)
(not
(modalAttribute
(not ?FORMULA) Permission)))
(=>
(modalAttribute ?FORMULA Permission)
(not
(modalAttribute
(not ?FORMULA) Obligation)))
(subclass Cleaning Process)
(subclass BrushingTeeth Cleaning)
(documentation BrushingTeeth EnglishLanguage "&%Cleaning several instances
of a &%Tooth of an &%Animal a &%Toothbrush.")
(=>
(instance ?BT BrushingTeeth)
(exists (?T ?TB ?A)
(and
(instance ?A Animal)
(instance ?TB ToothBrush)
(instance ?T Tooth)
(part ?T ?A)
(instrument ?BT ?TB)
(destination ?BT ?T))))
;; Prob1
(confersObligation
(=>
(instance ?D Day)
(exists (?BT)
(and
(instance ?BT BrushingTeeth)
(during ?BT (WhenFn ?D))
(agent ?BT Me))))
MyMom Me)
;; Prob2
(hasAuthorityOver MyMom Me)
;; from SUMO
;; call it SUMO2
(=>
(confersObligation ?FORMULA ?AGENT1 ?AGENT2)
(holdsObligation ?FORMULA ?AGENT2))
;; Prob3a
(=>
(holdsDuring ?T
(and
(hasAuthorityOver ?AUTH ?AG)
(confersObligation ?F ?AUTH ?AG)))
(holdsDuring ?T
(desires ?AG ?F)))
;; Prob3b
(=>
(and
(hasAuthorityOver ?AUTH ?AG)
(confersObligation (holdsDuring ?T ?F) ?AUTH ?AG))
(desires ?AG (holdsDuring ?T ?F)))
;; Prob3c
(=>
(and
(hasAuthorityOverT ?T ?AUTH ?AG)
(confersObligationT ?T ?F ?AUTH ?AG))
(desiresT ?T ?AG ?F))
;; Prob3d
(=>
(and
(hasAuthorityOver ?AUTH ?AG)
(confersObligation ?F ?AUTH ?AG))
(desires ?AG ?F))
;; Prob4
(=>
(holdsObligation ?F ?AG)
(modalAttribute ?F Obligation))
;; Prob5
(holdsRight
(exists (?D)
(not
(exists (?BT)
(and
(instance ?BT BrushingTeeth)
(during ?BT (WhenFn ?D))
(agent ?BT Me)))))
Me)
;; Todo: describe worlds and acc relns and then give
;; Kripki style translation to FO
;; AP- cool!
(=>
(modalAttribute ?FORMULA Obligation)
(modalAttribute ?FORMULA Permission))