[Attempto] RACE answers queries "how many" and "how much"

[Norbert E. Fuchs]

On 13 Apr 2012, at 24:29 , Norbert E. Fuchs wrote:

>> On 12 Apr 2012, at 23:27 , David Whitten wrote:
>> 
>> I tried the query:
>> Who is a woman and is not a human?
>> 
>> I got the answer:
>> Query cannot be answered.
>> 
>> I'm confused. Does RACE do queries that have negation?
> 
> I guess that the query should be answered from the axioms given as example on RACE's web-site, i.e. 
> 
> Every man is a human. Every woman is a human. Mary is a woman. John is a man.
> 
> 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.".

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


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."

Regards.

   --- nef 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20120413/0d211c4d/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2012-04-13 at 9.07.21 .png
Type: image/png
Size: 29367 bytes
Desc: not available
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20120413/0d211c4d/attachment-0001.png>