Thank you again Norbert for helping understand what RACE was attempting to communicate.<br>
<br>
With your indulgence I would ask If you could clarify a little more. <br>I asked the query expecting that there would be no solution<br>
to the query.  I think that from the statement "every woman is a human", <br>then this statement should be equivalent to the statement <br>that "there does not exist a woman who is not a human".<br><br>
How does RACE communicate that the set of facts satisfying the theorem<br>is empty ? <br><br>It doesn't seem to me that this is the same as saying that the <br>theorem doesn't follow from the axioms.  <br><br>If I said "the theorem doesn't follow from the axioms", <br>
I think I would mean that with a better set of axioms, <br>the ambiguity in the theorem would be removed and it would be <br>possible to prove the theorem from the axioms. Another way<br>to interpret it would be to say that the theorem is not in the<br>
deductive closure of the axioms.<br><br>I know that I haven't spent as much time in the field as some of the<br>other people on this list, so please enlighten me if I am not thinking clearly.<br><br>Best Wishes,<br>David Whitten<br>
713-870-3834<br><br><div class="gmail_quote">On Fri, Apr 13, 2012 at 3:27 AM, Norbert E. Fuchs <span dir="ltr"><<a href="mailto:fuchs@ifi.uzh.ch">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><div><div>On 13 Apr 2012, at 24:29 , Norbert E. Fuchs wrote:</div><div class="im"><br><blockquote type="cite"></blockquote><blockquote type="cite"><blockquote type="cite">On 12 Apr 2012, at 23:27 , David Whitten wrote:<br>
<br></blockquote></blockquote><blockquote type="cite"><div><blockquote type="cite">I tried the query:<br></blockquote><blockquote type="cite">Who is a woman and is not a human?<br></blockquote><blockquote type="cite"><br>
</blockquote><blockquote type="cite">I got the answer:<br></blockquote><blockquote type="cite">Query cannot be answered.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">I'm confused. Does RACE do queries that have negation?<br>
</blockquote><br>I guess that the query should be answered from the axioms given as example on RACE's web-site, i.e. <br><br>Every man is a human. Every woman is a human. Mary is a woman. John is a man.<br><br>RACE does answer queries containing negation, and the answer given is correct since the query cannot be deduced from the axioms. Maybe, you are confused by "Query cannot be answered." that perhaps should be replaced by "Query does not follow from axioms.".<font color="#007329"><br>
</font></div></blockquote><br></div></div><div>To shed more light on the situation, I replaced David's question "Who is a woman and is not a human?" by the theorem "There is a woman who is not a human." that – if we disregard the possible substitution of the query word "who" – generates the same proof. Here is the result</div>
<div><br></div><div><img src="cid:400BACB1-9CF7-451A-92D0-820C0C4C2864@uzh.ch" width="1077" height="188"></div><br><div>Here we get the unambiguous answer "Theorems do not follow from axioms." instead of the ambiguous "Query cannot be answered." that could be understood either as "Query does not follow from axioms." – which is intended – or as "RACE was not able do answer the query."</div>
<div><br></div><div>Regards.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>   --- nef </div></font></span></div><br>_______________________________________________<br>
attempto mailing list<br>
<a href="mailto:attempto@lists.ifi.uzh.ch">attempto@lists.ifi.uzh.ch</a><br>
<a href="https://lists.ifi.uzh.ch/listinfo/attempto" target="_blank">https://lists.ifi.uzh.ch/listinfo/attempto</a><br>
<br></blockquote></div><br>