From 8e5f4706712e05dcc26eb1731c43bd8828c157f9 Mon Sep 17 00:00:00 2001 From: Jean-Philippe Bernardy Date: Thu, 22 Nov 2018 14:21:35 +0100 Subject: [PATCH] complete analysis for sec 3 and 4 --- AnswerTypes.hs | 4 ++-- BankParser.hs | 2 +- Proofs.v | 11 +++++++++-- Tests.hs | 9 --------- 4 files changed, 12 insertions(+), 14 deletions(-) diff --git a/AnswerTypes.hs b/AnswerTypes.hs index c1bb24f..1322b40 100644 --- a/AnswerTypes.hs +++ b/AnswerTypes.hs @@ -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)] diff --git a/BankParser.hs b/BankParser.hs index 0a89473..8e83f40 100644 --- a/BankParser.hs +++ b/BankParser.hs @@ -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 diff --git a/Proofs.v b/Proofs.v index 6de67df..5b9cec8 100644 --- a/Proofs.v +++ b/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. @@ -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.*) @@ -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. diff --git a/Tests.hs b/Tests.hs index 0451e55..6b82575 100644 --- a/Tests.hs +++ b/Tests.hs @@ -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