Contact
CoCalc Logo Icon
StoreFeaturesDocsShareSupport News Sign UpSign In
| Download

Logic of "all" + verbs + relative clauses, for a class at Indiana University

Views: 6870
1
module AllVerbsRelativeClausesLM where
2
3
import Data.List
4
import Control.Monad
5
import Syntax2
6
import FrontEnd
7
import SyllogisticInference
8
import ExampleSentences
9
import ExampleRules
10
import ProofTreeNumbers
11
import Models
12
13
14
termEval x = semanticsTerm (head $ tF $ words x)
15
16
allVerbsIn gamma = nub $ concatMap verbsIn (readSs gamma)
17
18
tryOneStep z = applyAllRules z [antiARC, barbaraARC, axiom]
19
20
oneStepARC gammaWithReasons stopList =
21
let
22
z = dropReasons gammaWithReasons
23
a = map (applyARule z) [antiARC, barbaraARC,axiom] -- was antiARC
24
b = concat a
25
in
26
fixDuplicates $ gammaWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
27
28
29
filterAfterApply stopList x = [ s | s <- x, checkARC stopList s]
30
checkARC stopList (Sent d t u) = (t `elem` stopList)
31
32
fixedPointARC gammaWithReasons stopList = gammaWithReasons : map (\ x -> oneStepARC x stopList )(fixedPointARC gammaWithReasons stopList)
33
34
followsInARC phi gamma = followsInARCUnderRepresenatations (readS phi) (readSs gamma)
35
followsInARCUnderRepresenatations phi gamma =
36
let
37
ruleList = [axiom,barbaraARC,antiARC]
38
stopList = nub $ concatMap subterms (gamma ++ [phi])
39
withReasons = addReasonsToOriginal gamma -- this was the original line; don't lose it!
40
h = applyARule (gamma ++ [phi]) axiom -- new
41
withReason = withReasons ++ h
42
oneStepARC setWithReasons =
43
let
44
z = dropReasons setWithReasons
45
a = map (applyARule z) ruleList
46
b = concat a
47
in
48
fixDuplicates $ setWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
49
fixedPointARC = withReason : map oneStepARC fixedPointARC --- withReason had been withReasons !! note
50
firstRepeatOrFind (x:y:rest)
51
| phi `elem` (map get1 x) = do
52
putStrLn " "
53
putStrLn "The sentence follows, and here is a derivation in ARC from the assumptions:"
54
putStrLn " "
55
mapM_ print $ modify . full_reverse $ near $ tree_reverse $ proofSearch phi x
56
putStrLn " "
57
| x == y = do
58
{
59
putStrLn "The given sentence is not provable from the assumptions in ARC.";
60
putStrLn " ";
61
-- mapM_ print $ x ; -- !!
62
putStrLn "Here is a counter-model:";
63
countermod gamma phi stopList x;
64
}
65
| otherwise = firstRepeatOrFind (y:rest)
66
in firstRepeatOrFind fixedPointARC
67
68
69
justCounterModelARC p g =
70
let
71
phi = readS p
72
gamma = readSs g
73
ruleList = [axiom,barbaraARC,antiARC]
74
stopList = nub $ concatMap subterms (gamma ++ [phi])
75
withReasons = addReasonsToOriginal gamma
76
oneStepARC setWithReasons =
77
let
78
z = dropReasons setWithReasons
79
a = map (applyARule z) ruleList
80
b = concat a
81
in
82
fixDuplicates $ setWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
83
fixedPointARC = withReasons : map oneStepARC fixedPointARC
84
firstRepeatOrFind (x:y:rest)
85
| x == y = modelBuildARC stopList x -- countermod gamma phi stopList x
86
| otherwise = firstRepeatOrFind (y:rest)
87
in firstRepeatOrFind fixedPointARC
88
89
90
91
fullStoryARC phi gamma = fullStoryARCUnderRepresenatations (readS phi) (readSs gamma)
92
fullStoryARCUnderRepresenatations phi gamma =
93
let
94
ruleList = [axiom,barbaraARC,antiARC]
95
stopList = nub $ concatMap subterms (gamma ++ [phi])
96
withReasons = addReasonsToOriginal gamma
97
oneStepARC setWithReasons =
98
let
99
z = dropReasons setWithReasons
100
a = map (applyARule z) ruleList
101
b = concat a
102
in
103
fixDuplicates $ setWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
104
fixedPointARC = withReasons : map oneStepARC fixedPointARC
105
firstRepeatOrFind (x:y:rest)
106
| phi `elem` (map get1 x) = do
107
putStrLn " "
108
putStrLn "The sentence follows, and here is a derivation in ARC from the assumptions:"
109
putStrLn " "
110
mapM_ print $ modify . full_reverse $ near $ tree_reverse $ proofSearch phi x
111
putStrLn " "
112
| x == y = do
113
{
114
putStrLn "The given sentence is not provable from the assumptions in ARC.";
115
putStrLn " ";
116
putStrLn "Here is the list of sentences which do follow, and with restrictions:";
117
mapM_ print $ map get1 x
118
}
119
| otherwise = firstRepeatOrFind (y:rest)
120
in firstRepeatOrFind fixedPointARC
121
122
123
124
countermod gamma phi stpList chunk =
125
let
126
m = modelBuildARC stpList chunk -- !!!! USE THIS AND THIS ONLY FOR the FULL MODELS
127
-- mShortened = iterativelyShorten m (gamma++[negation phi]) -- !!!! PUT THIS BACK FOR SMALLER MODELS
128
129
in
130
showModelNounsVerbsPlusJustificationsARC m gamma phi stpList -- !!!! PUT THIS BACK FOR the FULL MODELS
131
-- showModelNounsVerbsPlusJustificationsARC mShortened gamma phi stpList -- !!! PUT THIS BACK FOR SMALLER MODELS
132
133
modelBuildARC stpList chunk =
134
let
135
k:: Int
136
k = length stpList
137
uni = [0..k-1]
138
sList = map get1 chunk
139
relVerbs = nub $ concatMap verbsIn sList
140
relevantCNs = nub $ concatMap cnsIn sList
141
withNumbers = zip stpList uni
142
order = map pairOfTerms sList
143
cnInterpretationFn cn = [ r | r<- uni, ((stpList !! r), (CNasTerm (PCN Pos cn) )) `elem` order]
144
tvInterpretationFn tv = [(r,s) | r<-uni, s<-uni, ((stpList!! r), (TermMaker (PV Pos tv) (TermNP All (stpList!! s)))) `elem` order]
145
termInterpretationFn t = (t, [r | r<-uni, ((stpList !! r),t) `elem` order])
146
m = Model {universe = uni, cnDict = [ (M p (cnInterpretationFn p)) | p <- relevantCNs],
147
verbDict = [ (Vb transverb (tvInterpretationFn transverb)) | transverb <- relVerbs] }
148
in
149
m -- showModelPlus m stpList
150
151
152
153
154
155
pairOfTerms (Sent d t u) = (t,u)
156
157
syntaxCheck :: String -> IO()
158
syntaxCheck x =
159
case (inARC (readS x)) of
160
(Just True) -> putStrLn $ "Looks good!"
161
(Just False) -> putStrLn $ "Sorry, not in the fragment of this notebook"
162
Nothing -> putStrLn $ "Sorry, invalid input"
163
164
165
-- Here is a test of the main example in Chapter 2
166
167
tSkunks = TermMaker sees (TermNP All (CNasTerm skunks) )
168
tMammals = TermMaker sees (TermNP All (CNasTerm mammals))
169
tChordates = TermMaker sees (TermNP All (CNasTerm chordates))
170
tSkunks2 = TermMaker sees (TermNP All tSkunks )
171
172
testCh2gamma= [
173
(Sent All (CNasTerm skunks) (CNasTerm chordates)),
174
(Sent All tMammals tSkunks2),
175
(Sent All tSkunks2 (CNasTerm mammals))]
176
testCh2phi = (Sent All tSkunks tChordates)
177
178
--followsInARCUnderRepresenatations testCh2phi testCh2gamma
179
180
tCh2gamma = [ "all skunks chordates",
181
"all see all mammals see all see all skunks",
182
"all see all see all skunks mammals",
183
"all mammals see all chordates" ]
184
tCh2phi = "all see all skunks see all chordates"
185
186
-- followsInARC tCh2phi tCh2gamma
187
188
-- The specific mapping to Chapter 2 is
189
-- skunks --> hawks
190
---chordates --> birds
191
-- mammals -> turtles
192
193
-- 0 hawks
194
-- 1 birds
195
-- 2 see all turtles
196
-- 3 turtles
197
-- 4 see all see all hawks
198
-- 5 see all hawks
199
-- 6 see all birds
200
201
202
203
-- here there
204
--- 0 1
205
--- 1 6
206
--- 2 5
207
--- 3
208
--- 4
209
--- 5
210
--- 6
211
212
test2 =
213
[ M Chordates [3,4],
214
M Birds [1,2,5],
215
M Skunks [2]
216
]
217
vTest2= [Vb Sees [(1,2),(1,3), (2,1), (2,5), (3,1), (3,3), (3,4), (3,5), (4,3), (4,4), (5,2), (5,3)],
218
Vb Loves [(1,1),(1,2), (1,3), (1,5), (2,1), (3,3), (5,2), (5,5)] ,
219
Vb Hates [(2,1),(3,4), (5,1), (5,2), (5,3), (5,4)]
220
]
221
222
223
model2 = Model {universe = [1,2,3,4,5], cnDict = test2, verbDict = vTest2}
224
225
--- A GOOD TEST IS BELOW
226
--- followsInARC "all who see all who hate all skunks see all who love all mammals" ["all mammals hate all skunks", "all skunks see all skunks", "all who love all mammals are skunks", "all boys see all who love all skunks", "all who see all boys are mammals"]
227
228
-- followsInARC "all who see all who hate all skunks see all who love all mammals" ["all mammals see all skunks", "all skunks see all skunks", "all who love all mammals are skunks", "all boys see all who love all skunks", "all who see all boys are mammals"]
229
230
-- followsInARC "all who see all who hate all skunks see all who love all mammals" ["all mammals hate all skunks", "all skunks see all skunks", "all who love all mammals are skunks", "all boys see all who love all skunks", "all who see all boys are mammals", "all who see all boys see all skunks", "all who see all skunks love all skunks"]
231
232
233
conclusion1 = "all who see all who hate all skunks see all who love all mammals"
234
assumptions1 = ["all mammals hate all skunks",
235
"all skunks see all skunks",
236
"all who love all mammals are skunks",
237
"all birds see all who love all skunks",
238
"all who see all birds are mammals"]
239
240
241
assumptions2 = ["all mammals hate all skunks",
242
"all skunks see all skunks",
243
"all who love all mammals are skunks",
244
"all birds see all who love all skunks",
245
"all who see all birds are mammals",
246
"all who see all birds see all skunks",
247
"all who see all skunks love all skunks"]
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278