Skip to content

Commit

Permalink
complete analysis for sec 3 and 4
Browse files Browse the repository at this point in the history
  • Loading branch information
jyp committed Nov 22, 2018
1 parent 10f6280 commit 8e5f470
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 14 deletions.
4 changes: 2 additions & 2 deletions AnswerTypes.hs
Expand Up @@ -5,8 +5,8 @@ data Answer = Yes | No | Unknown | Undef | Unclear String deriving (Eq,Show,Ord)

answers :: [(Int, Answer)]
answers = nubBy ((==) `on` fst) $ sortBy (compare `on` fst) $
[(119, Unknown)] -- because mary could have used someone else's workstation
[(181, Yes)] -- this works for the same reason 180 works.
[(119, Unknown) -- because mary could have used someone else's workstation
,(181, Yes)] -- this works for the same reason 180 works.
++ officialAnswers

officialAnswers :: [(Int,Answer)]
Expand Down
2 changes: 1 addition & 1 deletion BankParser.hs
Expand Up @@ -166,7 +166,7 @@ overrides _ = Nothing

disabledProblems :: [Int]
disabledProblems =
[137,171,172,191,192,193,194,195
[137,171,172
,216,217 -- syntax wrong: should be (john is (fatter politician than
-- bill)) not ((john is fatter politician) than bill)
,230,231,232,233,234,235,236,237,238,239,240,241,243,244,245 -- syntax wrong
Expand Down
11 changes: 9 additions & 2 deletions Proofs.v
@@ -1,8 +1,8 @@
Load FraCoq2.


Require Import Omega.

Require Import Omega.

Theorem T114a: Problem114aTrue. cbv. intros. destruct H. destruct H. exists x. split. exact H. exists (PN2object mary_PN). split. apply I. exact H0. Qed.

Expand Down Expand Up @@ -363,7 +363,7 @@ Theorem T186c: Problem186cTrue. cbv. intros. destruct H. firstorder. Qed. (**rea

Theorem T187d: Problem187dTrue. cbv. intros. destruct H. firstorder. Qed. (**reading d works**)

Theorem T188c: Problem188bTrue. cbv. firstorder. Qed.
Theorem T188c: Problem188cTrue. cbv. firstorder. Qed.
(**reading c works while it is supposed to be unknown! System does a good job I think**)
(* We never had a strict reading; however Jones is put into scope before the elliptic VP is evaluated.
And, it must be done this way in order to support 182, 185 at least.*)
Expand All @@ -374,5 +374,12 @@ Theorem T189a: Problem189aTrue. cbv. intros. destruct H. firstorder. Qed.
Theorem T190b: Problem190bTrue. cbv. intros. destruct H. firstorder. Qed. (**reading b works!**)


Theorem T192a: Problem192aTrue. cbv. firstorder. Abort All.
Theorem T192a: Problem192aFalse. cbv. firstorder. Abort All.

Theorem T194a: Problem194aTrue. cbv. firstorder. Abort All.
Theorem T194a: Problem194aFalse. cbv. firstorder. Abort All.


Theorem T196a: Problem196aTrue. cbv. intro. firstorder. Qed.

9 changes: 0 additions & 9 deletions Tests.hs
Expand Up @@ -96,17 +96,8 @@ ouch122 = debug (phrToEff s_122_4_h)

-- 155. Incorrect syntax (one anaphora not present, fixed now)

-- Analysis for 181. IMO it can be "yes" on some reading.

-- Analysis for 183. Strict identity not implemented.

-- Analysis for 190. Strict identity not implemented.

-- Analysis for 191-195.
-- a) I don't even understand the sentence
-- b) "They" could refer to any subset of object introduced in the environment. Potentially very expensive computationally.
-- (Potentially a lot of readings to deal with) --- see 127



-- EXTRA Anaphoric problems: 014, 016, 046, 078, 111, 113
Expand Down

0 comments on commit 8e5f470

Please sign in to comment.