<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><br class=""><blockquote type="cite" class="">On 11 Aug 2015, at 13:47 , David Whitten <<a href="mailto:whitten@netcom.com" class="">whitten@netcom.com</a>> wrote:<br class=""><br class="">I don't know what I have done wrong.<br class=""><br class="">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 class=""><br class="">I had the axiom set:<br class=""><br class="">Every man is a human. Every woman is a human. <br class="">Mary is a human that is a woman. John is a human that is a man. Mack is a human.<br class="">if a human is not provably a woman then the human is a man.<br class=""><br class="">I had the query:<br class=""><br class="">Who is a man and is a human?<br class=""><br class="">RACE said: overall time: 0.552 sec; RACE time: 0.04 sec<br class="">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 class=""><br class="">Query: Who is a man and is a human?<br class=""><br class="">Parameters: <br class=""><br class="">The following minimal subsets of the axioms answer the query:<br class=""><br class=""><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Subset 1<br class=""><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 3: Mary is a human that is a woman.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 6: If a human is not provably a woman then the human is a man.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Substitution: who = (at least 1) woman<br class=""></div></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Subset 2<br class=""><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 3: Mary is a human that is a woman.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 6: If a human is not provably a woman then the human is a man.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Substitution: who = Mary<br class=""></div></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Subset 3<br class=""><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 4: John is a human that is a man.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Substitution: who = John<br class=""></div></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Subset 4<br class=""><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 5: Mack is a human.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• 6: If a human is not provably a woman then the human is a man.<br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>• Substitution: who = Mack<br class=""></div></div><br class=""></blockquote><br class=""><div class="">David</div><div class=""><br class=""></div><div class="">I had suggested non-redundant axioms</div><div class=""><br class=""></div><div class=""> 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 class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class=""><br class=""></div><div class=""><img apple-inline="yes" id="CA34325A-A57A-478B-BB3B-A7FDF594A797" height="430" width="1115" apple-width="yes" apple-height="yes" src="cid:E159620F-431E-4F18-9456-60444A124209@uzh.ch" class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class=""><img apple-inline="yes" id="996FDEEA-B516-454C-AE7C-904CEB1E1348" height="416" width="1116" apple-width="yes" apple-height="yes" src="cid:A528F161-73DE-4532-8B1F-5D2EC3E04CF9@uzh.ch" class=""></div><div class=""><br class=""></div><div class="">while the combination "... not ... not provable P ..." is not accepted as being semantically identically to "P".</div><div class=""><br class=""></div><div class=""><img height="292" width="1118" apple-width="yes" apple-height="yes" apple-inline="yes" id="BF7B5E89-C9A1-408B-BFD6-9A9F669FE029" src="cid:404F9752-FA97-4735-B684-D92732689DC2@uzh.ch" class=""></div><div class=""><br class=""></div><div class="">Any comments or suggestions?</div><div class=""><br class=""></div><div class="">Best regards.</div><div class=""><br class=""></div><div class=""> --- nef</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""> </div></body></html>