blob: 4ab033f72ccaa9fdca096cc0ac49e9a93acd171e (
plain) (
blame)
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
|
;;; Logic problem inference system
;;; Hybrid version: inference and backtracking
;; If you wrote procedure FOO to solve a problem in the inference
;; version, say SOLVE [FOO] to solve it in this version!
;; MAKE "SHORT "TRUE to eliminate printing new facts
;; MAKE "LONG "TRUE to add printing new implications
to solve :problem
if not namep "short [localmake "short "false]
if not namep "long [localmake "long "false]
localmake "indent 0
localmake "message runresult [catch "contradiction :problem]
if not emptyp :message [print :message]
end
;; Establish categories
to category :category.name :members
print (list "category :category.name :members)
if not namep "categories [make "categories []]
make "categories lput :category.name :categories
make :category.name :members
foreach :members [pprop ? "category :category.name]
end
;; Verify and falsify matches
to verify :a :b
settruth :a :b "true
end
to falsify :a :b
settruth :a :b "false
end
to settruth :a :b :truth.value
if equalp (gprop :a "category) (gprop :b "category) [stop]
localmake "oldvalue get :a :b
if equalp :oldvalue :truth.value [stop]
if equalp :oldvalue (not :truth.value) ~
[(throw "contradiction (sentence [inconsistency in settruth]
:a :b :truth.value))]
if not :short [indent print (list :a :b "-> :truth.value)]
store :a :b :truth.value
settruth1 :a :b :truth.value
settruth1 :b :a :truth.value
if not emptyp :oldvalue ~
[foreach (filter [equalp first ? :truth.value] :oldvalue)
[apply "settruth butfirst ?]]
end
to settruth1 :a :b :truth.value
apply (word "find not :truth.value) (list :a :b)
foreach (gprop :a "true) [settruth ? :b :truth.value]
if :truth.value [foreach (gprop :a "false) [falsify ? :b]
pprop :a (gprop :b "category) :b]
pprop :a :truth.value (fput :b gprop :a :truth.value)
end
to findfalse :a :b
foreach (filter [not equalp get ? :b "true] peers :a) ~
[falsify ? :b]
end
to findtrue :a :b
if equalp (count peers :a) (1+falses :a :b) ~
[verify (find [not equalp get ? :b "false] peers :a)
:b]
end
to falses :a :b
output count filter [equalp "false get ? :b] peers :a
end
to peers :a
output thing gprop :a "category
end
to indent
repeat :indent [type "| |]
end
;; Common types of clues
to differ :list
print (list "differ :list)
foreach :list [differ1 ? ?rest]
end
to differ1 :a :them
foreach :them [falsify :a ?]
end
to neighbor :this :that :lineup
falsify :this :that
implies :this first :lineup "true :that first bf :lineup "true
implies :that first :lineup "true :this first bf :lineup "true
implies :this last :lineup "true :that last bl :lineup "true
implies :that last :lineup "true :this last bl :lineup "true
neighbor1 :lineup count :lineup
end
to neighbor1 :lineup :count
if :count=0 [stop]
foreach (bf bf bf :lineup) [
implies :this first bf :lineup "true :that ? "false
implies :that first bf :lineup "true :this ? "false
]
neighbor1 (lput first :lineup bf :lineup) :count-1
end
to justbefore :this :that :lineup
falsify :this :that
falsify :this last :lineup
falsify :that first :lineup
justbefore1 :this :that :lineup
end
to justbefore1 :this :that :slotlist
if emptyp butfirst :slotlist [stop]
equiv :this (first :slotlist) :that (first butfirst :slotlist)
justbefore1 :this :that (butfirst :slotlist)
end
;; Remember conditional linkages
to implies :who1 :what1 :truth1 :who2 :what2 :truth2
localmake "old1 get :who1 :what1
if equalp :old1 :truth1 [settruth :who2 :what2 :truth2 stop]
if equalp :old1 (not :truth1) [stop]
localmake "old2 get :who2 :what2
if equalp :old2 :truth2 [stop]
if equalp :old2 (not :truth2) [settruth :who1 :what1 (not :truth1) stop]
if memberp (list :truth1 :who2 :what2 (not :truth2)) :old1 ~
[settruth :who1 :what1 (not :truth1) stop]
if memberp (list :truth1 :what2 :who2 (not :truth2)) :old1 ~
[settruth :who1 :what1 (not :truth1) stop]
if memberp (list (not :truth1) :who2 :what2 :truth2) :old1 ~
[settruth :who2 :what2 :truth2 stop]
if memberp (list (not :truth1) :what2 :who2 :truth2) :old1 ~
[settruth :who2 :what2 :truth2 stop]
if :long [indent
pr (se "|(| :who1 :what1 :truth1 "-> :who2 :what2 :truth2 "|)|)]
store :who1 :what1 ~
fput (list :truth1 :who2 :what2 :truth2) :old1
store :who2 :what2 ~
fput (list (not :truth2) :who1 :what1 (not :truth1)) :old2
end
to equiv :who1 :what1 :who2 :what2
implies :who1 :what1 "true :who2 :what2 "true
implies :who2 :what2 "true :who1 :what1 "true
end
to xor :who1 :what1 :who2 :what2
implies :who1 :what1 "true :who2 :what2 "false
implies :who1 :what1 "false :who2 :what2 "true
end
;; Interface to property list mechanism
to get :a :b
output gprop :a :b
end
to store :a :b :val
pprop :a :b :val
pprop :b :a :val
end
;; Backtrack if necessary
to solution
localmake "stack []
localmake "size (count thing first :categories)
localmake "number (count :categories)-1
catch "solved [try.solution]
end
to try.solution
if solvedp [print [] print.solution throw "solved]
foreach get.assumptions ~
[if not wordp (get first ? last ?)
[save.state
localmake "indent :indent+2
make "message runresult [catch "contradiction [make.assumption ?
try.solution]]
if not emptyp :message [indent print :message]
indent print (sentence "Assumption ? "failed)
restore.state
make "indent :indent-2
if not emptyp :message [falsify first ? last ?]
if solvedp [print [] print.solution throw "solved]]]
end
to solvedp
foreach thing first :categories [if not equalp :number count gprop ? "true
[output "false]]
output "true
end
to save.state
push "stack map [list ? plist ?] map.se "thing :categories
end
to restore.state
erpls
foreach pop "stack [setplist first ? last ?]
end
to setplist :name :list
if emptyp :list [stop]
pprop :name first :list first butfirst :list
setplist :name butfirst butfirst :list
end
to get.assumptions
localmake "array array :size
foreach (thing first :categories) ~
[[this] foreach (butfirst :categories)
[[that] assume]]
op map.se [item ? :array] iseq 1 :size
end
to assume ;; implicit arguments THIS (an individual) and THAT (a category)
if wordp gprop :this :that [stop]
localmake "tries filter [not wordp gprop :this ?] thing :that
localmake "slot count :tries
foreach :tries [setitem :slot :array fput (list :this ?) (item :slot :array)]
end
to make.assumption :assume
print [] indent print sentence "Assuming :assume
verify first :assume last :assume
end
;; Print the solution
to print.solution
foreach thing first :categories [solve1 ? butfirst :categories]
end
to solve1 :who :order
type :who
foreach :order [type "| | type gprop :who ?]
print []
end
;; Get rid of old problem data
to cleanup
if not namep "categories [stop]
ern :categories
ern "categories
erpls
end
|