The original submission did not include Justification with Gricean compressions. These have been added on 2007.06.01 in light of reviewer comments. The Justification with Gricean compressions cannot be certified or machine-verified, and are valid only because of the existence of the proofs corresponding to them -- proofs which can be verified. These arguments are included only because we came to understand that justifications are assessed on the basis of Gricean maxims (and the like) known to be in conflict with objective standards for normatively correct reasoning, rather than on the basis of such standards.
Download the submission file (.txt)
[578] [227] [286] [70] [581] [570] [550] [470] [452] [455]
<pair id="578" entailment="NO" task="QA" length="short">
<t>Io is 2,236 miles (3,598 kilometers) in diameter, slightly larger than the Earth's moon.</t>
<h>The terrestrial moon has a diameter of 3746 kilometers.</h>
</pair>
Since Earth's moon is the terrestrial moon, and Io, with a diameter of 3,598 kilometers, is larger than Earth's moon, the terrestrial moon cannot have a diameter of 3,746 kilometers.
1 578 NO
<just>
If planet x has a diameter n slightly larger than the diameter m of planet y, then n is greater than m. From t, we know that Io, a planet, has a diameter of 3598 kilometers. We also know from t that Io has a diameter that is slightly larger than that of Earth's moon. Therefore, Io has a diameter that is greater than the diameter of Earth's moon. Since the terrestrial moon is Earth's moon, we know from h that Earth's moon has a diameter of 3746. Therefore, we can deduce that 3598 is greater than 3746. But it's not the case that 3598 is greater than 3746. We have thus arrived at a contradiction. QED
</just>
(domains Orbs)
(declare (Io Earth TerrestrialMoon) Orbs)
(declare DiameterOf (-> (Orbs) Num))
(declare MoonOf (-> (Orbs) Orbs))
(declare greater-than (-> (Num Num) Boolean))
(define tacit
(and (= TerrestrialMoon (MoonOf Earth))
(not (greater-than 3598 3746))))
(define text
(and (= (DiameterOf Io) 3598)
(greater-than (DiameterOf Io) (DiameterOf (MoonOf Earth)))))
(define hypothesis
(= (DiameterOf TerrestrialMoon) 3746))
(assert [tacit text])
(suppose-absurd hypothesis
(dseq
(!sym (!left-and tacit))
(!fcong (= (DiameterOf (MoonOf Earth)) (DiameterOf TerrestrialMoon)))
(!left-and text)
(!right-and text)
(!rcong
(greater-than (DiameterOf Io) (DiameterOf (MoonOf Earth)))
(greater-than 3598 (DiameterOf TerrestrialMoon)))
(!reflex 3598)
(!rcong
(greater-than 3598 (DiameterOf TerrestrialMoon))
(greater-than 3598 3746))
(!absurd
(greater-than 3598 3746) (!right-and tacit2))))
<pair id="227" entailment="YES" task="IR" length="short" > <t>British mountaineer Alison Hargreaves becomes the first woman to climb Mount Everest alone and without oxygen tanks.</t> <h>A woman succeeds in climbing Everest solo.</h> </pair>
Since climbing alone means climbing solo, and Hargreaves climbed Everest alone, the hypothesis follows.
2 227 YES
<just>
Alison Hargreaves (who we can denote by 'a') has a number of attributes, according to the given proposition. For example, we can immediately deduce that a is a woman, and that a climbed Mount Everest (which we can denote by 'e') alone. Given that if x climbed y alone, x climbed y solo, we can deduce that a climbed e solo. Given as well that if x climbed y solo, x succeeds in climbing y solo, we can deduce that a succeeds in climbing e solo. By generalization, we can now deduce that there exists an x such that x is a woman, and x succeeds in climbing e solo. QED
</just>
(domains Person Mountain)
(declare (British Woman) (-> (Person) Boolean))
(declare (ClimbedAlone ClimbedWithoutTanks)
(-> (Person Mountain) Boolean))
(declare Alison-Hargreaves Person)
(declare Mount-Everest Mountain)
(define-symbol ClimbedSolo
(forall ?x ?y
(iff (ClimbedSolo ?x ?y)
(ClimbedAlone ?x ?y))))
(define text
(and (British Alison-Hargreaves)
(Woman Alison-Hargreaves)
(ClimbedAlone Alison-Hargreaves Mount-Everest)
(ClimbedWithoutTanks Alison-Hargreaves Mount-Everest)))
(define goal
(exists ?x
(and (Woman ?x)
(ClimbedSolo ?x Mount-Everest))))
(assert text)
(dlet ((w (!left-and (!right-and text)))
(ca (!left-and (!right-and (!right-and text))))
(cs (!mp (!right-iff
(!uspec*
(forall ?x ?y
(iff (ClimbedSolo ?x ?y)
(ClimbedAlone ?x ?y)))
[Alison-Hargreaves Mount-Everest]))
ca))
(h (!both w cs)))
(!egen goal Alison-Hargreaves))
<pair id="286" entailment="YES" task="IR" length="short" >
<t>Italian film-maker, Fellini was awarded an honorary Oscar for lifetime achievement. He died on October 31, 1993.</t>
<h>An Italian director is awarded an honorary Oscar.</h>
</pair>
Since film-makers are directors, and Fellini is a film-maker who was awarded an honorary Oscar, the hypothesis is entailed.
3 286 YES
<just>
It follows immediately from the first sentence in the premise that the following conjunction holds: Fellini was Italian, was a film-maker, and was awarded an honorary Oscar. Since from any conjunction each of the elements conjoined can be inferred, it can be inferred in this case that Fellini was a film-maker. Since if x is a film-maker, x is a director, it follows that Fellini was a director. Assembling a new conjunction, we can deduce that Fellini was Italian, was a director, and was awarded an honorary Oscar. Generalizing, we can from this deduce that an Italian director was awarded an honorary Oscar. QED
</just>
(domains Person Time)
(declare (Film-Maker Director Italian Oscar-Winner)
(-> (Person) Boolean))
(declare Died (-> (Person Time) Boolean))
(declare Fellini Person)
(declare Oct-31-1993 Time)
(define tacit
(forall ?x
(iff (Director ?x)
(Film-Maker ?x))))
(define text
(and (and (Italian Fellini)
(and (Film-Maker Fellini)
(Oscar-Winner Fellini)))
(Died Fellini Oct-31-1993)))
(define hypothesis
(exists ?x
(and (Italian ?x)
(and (Director ?x)
(Oscar-Winner ?x)))))
(assert tacit)
(assert text)
(dlet ((sen1 (!left-and text))
(fellini-is-italian (!left-and sen1))
(fellini-is-film-maker (!left-and (!right-and sen1)))
(fellini-is-director (!mp (!right-iff (!uspec tacit Fellini))
fellini-is-film-maker))
(fellini-won-oscar (!right-and (!right-and sen1)))
(hyp (!both fellini-is-italian
(!both fellini-is-director
fellini-won-oscar))))
(hypothesis BY (!egen hypothesis Fellini)))
<pair id="70" entailment="YES" task="IE" length="short" > <t>Hughes loved his wife, Gracia, and was absolutely obsessed with his little daughter Elicia.</t> <h>Hughes was married to Gracia.</h> </pair>
Since everyone who has a wife is married to that wife, the hypothesis is entailed.
4 70 YES
<just>
We can deduce from the premise that Hughes loved his wife, Gracia. (This is just one of the two conjuncts in the premise, after all.) We know that if x loved y, where y is the wife of x, then y was the wife of x. We can therefore deduce that Gracia was the wife of Hughes.
We also know that if x was the wife of y, then y was married to x. Thus we can deduce that Hughes was married to Gracia. QED
</just>
(domain Person)
(declare (Hughes Gracia Elicia) Person)
(declare (Loved HusbandOf WifeOf DaughterOf ObsessedWith)
(-> (Person Person) Boolean))
(declare (Little) (-> (Person) Boolean))
(define-symbol Married
(forall ?x ?y
(iff (Married ?x ?y)
(or (WifeOf ?x ?y)
(HusbandOf ?x ?y)))))
(define text
(and (WifeOf Hughes Gracia)
(Loved Hughes Gracia)
(DaughterOf Hughes Elicia)
(ObsessedWith Hughes Elicia)))
(define goal
(Married Hughes Gracia))
(assert text)
(dlet ((p1 (!left-and text))
(p2 (!either (WifeOf Hughes Gracia)
(HusbandOf Hughes Gracia)))
(p3 (!uspec* (forall ?x ?y
(iff (Married ?x ?y)
(or (WifeOf ?x ?y)
(HusbandOf ?x ?y))))
[Hughes Gracia])))
(goal BY (!mp (!right-iff p3) p2)))
<pair id="581" entailment="YES" task="QA" length="short">
<t>Two prominent scientists have made guest appearances on the show,
paleontologist Stephen Jay Gould and Stephen Hawking, the theoretical
physicist whose brilliance has been compared with Einstein's.</t>
<h>Stephen Hawking is a physicist.</h>
</pair>
Because Hawking is a theoretical physicist, and all such people are obviously physicists, the hypothesis is entailed.
5 581 YES
<just>
We know from t that Stephen Jay Gould has made guest appearances on the show, that Stephen Hawking has made guest appearances on the show, that Stephen Hawking is a theoretical physicist, and that Stephen Hawking's brilliance has been compared with Einstein's. It follows that Stephen Hawking is a theoretical physicist. If x is a theoretical physicist, x is a physicist. Therefore, Stephen Hawking is a physicist. QED
</just>
(domains Shows People Brilliance)
(declare (AlbertEinstein StephenJayGould StephenHawking) People)
(declare TheShow Shows)
(declare (Scientist Paleontologist TheoreticalPhysicist Physicist)
(-> (People) Boolean))
(declare ComparedWith (-> (Brilliance Brilliance) Boolean))
(declare BrillianceOf (-> (People) Brilliance))
(declare AppearedOn (-> (People Shows) Boolean))
(define tacit
(forall ?x
(if (TheoreticalPhysicist ?x)
(Physicist ?x))))
(define text
(and (AppearedOn StephenJayGould TheShow)
(AppearedOn StephenHawking TheShow)
(Paleontologist StephenJayGould)
(TheoreticalPhysicist StephenHawking)
(ComparedWith (BrillianceOf StephenHawking)
(BrillianceOf AlbertEinstein))))
(define hypothesis
(Physicist StephenHawking))
(assert [tacit text])
(hypothesis
BY
(!mp (!uspec tacit StephenHawking)
(!left-and
(!right-and
(!right-and
(!right-and text))))))
<pair id="570" entailment="YES" task="QA" length="short"> <t>President Bill Clinton on Tuesday passed the leadership of the Democratic Party to Vice President Al Gore, describing his deputy as the right person to be the first U.S. President of the 21st century.</t> <h>Bill Clinton belongs to the Democratic Party.</h> </pair>
Since the leader of a political party belongs to that party, and Clinton was the leader of the Democratic Party, the hypothesis is entailed.
6 570 YES
<just>
From t we know that President Bill Clinton on Tuesday passed the leadership of the Democratic Party to Vice President Al Gore, and that Bill Clinton described his deputy as the right person to be the first U.S. President of the 21st century. If person x on day D passes the leadership of a political party P to person y, x belongs to P. Therefore, Bill Clinton belongs to the Democratic Party. QED
</just>
(domains Person Party Leadership) (declare LeadershipOf (-> (Party) Leadership)) (declare (BillClinton AlGore) Person) (declare DemocraticParty Party) (declare PassedOnTo (-> (Person Leadership Person) Boolean)) (declare BelongsTo (-> (Person Party) Boolean)) (define tacit (forall ?x ?y ?z (if (PassedOnTo ?x (LeadershipOf ?y) ?z) (and (BelongsTo ?x ?y) (BelongsTo ?z ?y))))) (define text (PassedOnTo BillClinton (LeadershipOf DemocraticParty) AlGore)) (define hypothesis (BelongsTo BillClinton DemocraticParty)) (assert [tacit text]) (hypothesis BY (!left-and (!mp (!uspec* tacit [BillClinton DemocraticParty AlGore]) text)))
<pair id="550" entailment="YES" task="QA" length="short"> <t>Bukowski attracted the attention of John Martin who founded Black Sparrow Press in 1965 specifically to publish him.</t> <h>John Martin is the founder of Black Sparrow Press.</h> </pair>
Since anyone who founded an organization is obviously the founder of it, and Martin founded Black Sparrow Press, the hypothesis is entailed.
7 550 YES
<just>
From t we know that Bukowski attracted the
attention of John Martin, and that John Martin founded Black Sparrow Press in 1965, and that John Martin found Black Sparrow Press in 1965 in order to publish Bukowski. It follows directly from the second of these conjuncts that John Martin founded Black Sparrow Press in 1965. If x founded an organization O in year n, then x is the founder of O. It follows that John Martin is the founder of Black Sparrow Press. QED
</just>
(domains Person Organization Attention)
(declare Attracted (-> (Person Attention) Boolean))
(declare AttentionOf (-> (Person) Attention))
(declare FoundedIn (-> (Person Organization Num) Boolean))
(declare Founded (-> (Person Organization) Boolean))
(declare FounderOf (-> (Organization) Person))
(declare (Bukowski JohnMartin) Person)
(declare BlackSparrowPress Organization)
(define tacit
(forall ?x ?y ?z
(if (FoundedIn ?x ?y ?z)
(= (FounderOf ?y) ?x))))
(define text
(and (Attracted Bukowski (AttentionOf JohnMartin))
(FoundedIn JohnMartin BlackSparrowPress 1965)))
(define hypothesis
(= JohnMartin (FounderOf BlackSparrowPress)))
(assert [tacit text])
(hypothesis
BY
(!sym (!mp (!uspec* tacit [JohnMartin BlackSparrowPress 1965])
(!right-and text))))
<pair id="470" entailment="YES" task="QA" length="short"> <t>Gabriel Garcia Marquez is the author of "One Hundred Years of Solitude", "The Autumn of the Patriarch" and other novels.</t> <h>Gabriel Garcia Marquez is a novelist and writer.</h> </pair>
Because authors are writers, and Marquez is the author of novels, the hypothesis is entailed.
8 470 YES
<just>
From t we know that Gabriel Garcia Marquez is the author of the novel ``One Hundred Years of Solitude,'' is the author of the novel ``The Autumn of the Patriach,'' and is the author of at least two additional novels. We can directly infer that Gabriel Garcia Marquez is the author of the novel ``One Hundred Years of Solitude.'' If x is the author of the novel b, then x is a novelist and writer. It follows that Gabriel Garcia Marquez is a novelist and writer. QED
</just>
(domains Person Novel)
(declare Gabrial-Garcia-Marquez Person)
(declare One-Hundred-Years-Of-Solitude Novel)
(declare The-Autumn-Of-The-Patriach Novel)
(declare author-of (-> (Person Novel) Boolean))
(declare author (-> (Person) Boolean))
(declare novelist (-> (Person) Boolean))
(define tacit
(forall ?person ?novel
(if (author-of ?person ?novel) (and (novelist ?person) (author ?person)))))
(define text
(and (author-of Gabrial-Garcia-Marquez One-Hundred-Years-Of-Solitude)
(author-of Gabrial-Garcia-Marquez The-Autumn-Of-The-Patriach)
(exists ?x ?y
(and (not (or (= ?x ?y)
(= ?x One-Hundred-Years-Of-Solitude)
(= ?y One-Hundred-Years-Of-Solitude)
(= ?x The-Autumn-Of-The-Patriach)
(= ?y The-Autumn-Of-The-Patriach)))
(author-of Gabrial-Garcia-Marquez ?x)
(author-of Gabrial-Garcia-Marquez ?y)))))
(define hypothesis
(and (novelist Gabrial-Garcia-Marquez)
(author Gabrial-Garcia-Marquez)))
(assert [tacit text])
(hypothesis BY
(!mp (!uspec (!uspec tacit Gabrial-Garcia-Marquez) One-Hundred-Years-Of-Solitude)
(!left-and text)))
<pair id="452" entailment="YES" task="QA" length="short">
<t>Boris Becker is a true legend in the sport of tennis. Aged just
seventeen, he won Wimbledon for the first time and went on to become the
most prolific tennis player.</t>
<h>Boris Becker is a Wimbledon champion.</h>
</pair>
Because someone who wins Wimbledon is a Wimbledon champion, and Becker won this tournament, the hypothesis is entailed.
9 452 YES
<just>
From the second sentence of t we can deduce that Boris Becker won Wimbledon at 17 years of age, and that Boris Becker went on to become the most prolific tennis player. If x won Wimbledon at n years of age, then x is a Wimbleton champion. Therefore, Boris Becker is a Wimbledon champion. QED
</just>
(domains Person Age Action)
(declare Boris-Becker Person)
(declare seventeen Age)
(declare won-wimbledon Action)
(declare performed-action-at-age (-> (Person Action Age) Boolean))
(declare performed-action (-> (Person Action) Boolean))
(declare wimbledon-champion (-> (Person) Boolean))
(declare became-prolific-tennis-player (-> (Person) Boolean))
(define tacit1
(forall ?person ?action ?age
(if (performed-action-at-age ?person ?action ?age)
(performed-action ?person ?action))))
(define tacit2
(forall ?person
(if (performed-action ?person won-wimbledon)
(wimbledon-champion ?person))))
(define text
(and (performed-action-at-age Boris-Becker won-wimbledon seventeen)
(became-prolific-tennis-player Boris-Becker)))
(define hypothesis
(wimbledon-champion Boris-Becker))
(assert [tacit1 tacit2 text])
(hypothesis BY
(!mp
(!uspec tacit2 Boris-Becker)
(!mp (!uspec (!uspec (!uspec tacit1 Boris-Becker) won-wimbledon) seventeen)
(!left-and text))))
<pair id="455" entailment="YES" task="QA" length="short"> <t>He interviewed Shigeko Sasamori in December 2004. Ms. Sasamori was thirteen when the atomic bomb was dropped on Hiroshima (August 6, 1945).</t> <h>In 1945, an atomic bomb was dropped on Hiroshima.</h> </pair>
Since the atomic bomb was dropped on Hiroshima on the particular date of August 6, 1945, which is obviously in the year 1945, the hypothesis is entailed.
10 455 YES
<just>
If x was n years of age when e occurred (month day year), then in year, event e occurred. From the second sentence of t, and this rule, it follows that in 1945, the atomic bomb was dropped on Hiroshima. It follows that in 1945, an atomic bomb was dropped on Hiroshima. QED
</just>
(domains Person Event Bomb Location Date)
(declare ShigekoSasamori Person)
(declare Hiroshima Location)
(declare TheAtomicBomb Bomb)
(declare AtomicBomb (-> (Bomb) Boolean))
(declare DroppingEvent (-> (Bomb Location) Event))
(declare AgeOfAtEvent (-> (Person Event) Num))
(declare DateOfEvent (-> (Event) Date))
(declare YYMMDD (-> (Num Num Num) Date))
(define tacit
(AtomicBomb TheAtomicBomb))
(define text
(and (= (AgeOfAtEvent ShigekoSasamori (DroppingEvent TheAtomicBomb Hiroshima)) 13)
(= (DateOfEvent (DroppingEvent TheAtomicBomb Hiroshima)) (YYMMDD 1945 8 6))))
(define hypothesis
(exists ?bomb ?month ?day
(and (AtomicBomb ?bomb)
(= (DateOfEvent (DroppingEvent ?bomb Hiroshima)) (YYMMDD 1945 ?month ?day)))))
(assert [tacit text])
(hypothesis
BY
(dseq
(!both tacit
(!right-and text))
(!egen
(exists ?day
(and (AtomicBomb TheAtomicBomb)
(= (DateOfEvent (DroppingEvent TheAtomicBomb Hiroshima)) (YYMMDD 1945 8 ?day))))
6)
(!egen
(exists ?month ?day
(and (AtomicBomb TheAtomicBomb)
(= (DateOfEvent (DroppingEvent TheAtomicBomb Hiroshima)) (YYMMDD 1945 ?month ?day))))
8)
(!egen
(exists ?bomb ?month ?day
(and (AtomicBomb ?bomb)
(= (DateOfEvent (DroppingEvent ?bomb Hiroshima)) (YYMMDD 1945 ?month ?day))))
TheAtomicBomb)))
