<div dir="ltr"><div><div><div>Norbert,<br></div>thank you for the hard work on RACE.<br></div>I did use the interface at <a href="http://attempto.ifi.uzh.ch/race/">http://attempto.ifi.uzh.ch/race/</a><br></div>and got results that I expected:<br><br><div class="in"><p><b>Axioms</b>: Every man is a human. Every woman is a human.
Mary is a woman. John is a man. Kelly is a human.
if a human is not provably a woman then the human is a man.
</p><p><b>Theorems</b>: Kelly is a woman.</p><p><b>Parameters</b>: </p></div><p>Theorems do not follow from axioms.</p><div class="infoBox">overall time: 0.585 sec; RACE time: 0.024 sec</div><div class="in"><p><b>Axioms</b>: Every man is a human. Every woman is a human.
Mary is a woman. John is a man. Kelly is a human.
if a human is not provably a woman then the human is a man.
</p><p><b>Theorems</b>: Kelly is a man.</p><p><b>Parameters</b>: </p></div><p>The following minimal subsets of the axioms entail the theorems:</p>Subset 1<ul><li>5: Kelly is a human.</li><li>6: If a human is not provably a woman then the human is a man.</li></ul><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Aug 17, 2015 at 12:32 PM, Norbert E. Fuchs <span dir="ltr"><<a href="mailto:fuchs@ifi.uzh.ch" target="_blank">fuchs@ifi.uzh.ch</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><br><blockquote type="cite">On 11 Aug 2015, at 13:47 , David Whitten <<a href="mailto:whitten@netcom.com" target="_blank">whitten@netcom.com</a>> wrote:<br><br>I don't know what I have done wrong.<br><br>I tried using the web interface for race, but don't know why (below) subset #1 (Mary) and set#2 (at least 1 woman) are included.<br><br>I had the axiom set:<br><br>Every man is a human. Every woman is a human. <br>Mary is a human that is a woman. John is a human that is a man. Mack is a human.<br>if a human is not provably a woman then the human is a man.<br><br>I had the query:<br><br>Who is a man and is a human?<br><br>RACE said: overall time: 0.552 sec; RACE time: 0.04 sec<br>Axioms: Every man is a human. Every woman is a human. Mary is a human that is a woman. John is a human that is a man. Mack is a human. if a human is not provably a woman then the human is a man.<br><br>Query: Who is a man and is a human?<br><br>Parameters: <br><br>The following minimal subsets of the axioms answer the query:<br><br><div><span style="white-space:pre-wrap"> </span>• Subset 1<br><div><span style="white-space:pre-wrap"> </span>• 3: Mary is a human that is a woman.<br></div><div><span style="white-space:pre-wrap"> </span>• 6: If a human is not provably a woman then the human is a man.<br></div><div><span style="white-space:pre-wrap"> </span>• Substitution: who = (at least 1) woman<br></div></div><div><span style="white-space:pre-wrap"> </span>• Subset 2<br><div><span style="white-space:pre-wrap"> </span>• 3: Mary is a human that is a woman.<br></div><div><span style="white-space:pre-wrap"> </span>• 6: If a human is not provably a woman then the human is a man.<br></div><div><span style="white-space:pre-wrap"> </span>• Substitution: who = Mary<br></div></div><div><span style="white-space:pre-wrap"> </span>• Subset 3<br><div><span style="white-space:pre-wrap"> </span>• 4: John is a human that is a man.<br></div><div><span style="white-space:pre-wrap"> </span>• Substitution: who = John<br></div></div><div><span style="white-space:pre-wrap"> </span>• Subset 4<br><div><span style="white-space:pre-wrap"> </span>• 5: Mack is a human.<br></div><div><span style="white-space:pre-wrap"> </span>• 6: If a human is not provably a woman then the human is a man.<br></div><div><span style="white-space:pre-wrap"> </span>• Substitution: who = Mack<br></div></div><br></blockquote><br><div>David</div><div><br></div><div>I had suggested non-redundant axioms</div><div><br></div><div> Every man is a human. Every woman is a human. Mary is a woman. John is a man. Mack is a human. If a human is not provably a woman then the human is a man.</div><div><br></div><div>and asked you for patience while I was about to remove a bug that prevented your example from executing. In the meantime I removed the bug and now get the expected result seen here in a screen-shot of RACE's web-interface.</div><div><br></div><div><br></div><div><img src="cid:E159620F-431E-4F18-9456-60444A124209@uzh.ch" height="430" width="1115"></div><div><br></div><div><br></div><div>Also, I extended RACE to handle the combination of logical negation ("not") and negation-as-failure ("not provable"). Here is an example of "... not provable ... not ..." </div><div><br></div><div><img src="cid:A528F161-73DE-4532-8B1F-5D2EC3E04CF9@uzh.ch" height="416" width="1116"></div><div><br></div><div>while the combination "... not ... not provable P ..." is not accepted as being semantically identically to "P".</div><div><br></div><div><img src="cid:404F9752-FA97-4735-B684-D92732689DC2@uzh.ch" height="292" width="1118"></div><div><br></div><div>Any comments or suggestions?</div><div><br></div><div>Best regards.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div> --- nef</div><div><br></div><div><br></div><div> </div></font></span></div></blockquote></div><br></div>