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

[David Whitten]

Thank you again Norbert for helping understand what RACE was attempting to
communicate.

With your indulgence I would ask If you could clarify a little more.
I asked the query expecting that there would be no solution
to the query.  I think that from the statement "every woman is a human",
then this statement should be equivalent to the statement
that "there does not exist a woman who is not a human".

How does RACE communicate that the set of facts satisfying the theorem
is empty ?

It doesn't seem to me that this is the same as saying that the
theorem doesn't follow from the axioms.

If I said "the theorem doesn't follow from the axioms",
I think I would mean that with a better set of axioms,
the ambiguity in the theorem would be removed and it would be
possible to prove the theorem from the axioms. Another way
to interpret it would be to say that the theorem is not in the
deductive closure of the axioms.

I know that I haven't spent as much time in the field as some of the
other people on this list, so please enlighten me if I am not thinking
clearly.

Best Wishes,
David Whitten
713-870-3834

On Fri, Apr 13, 2012 at 3:27 AM, Norbert E. Fuchs <fuchs at ifi.uzh.ch> wrote:

>
> 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
>
> _______________________________________________
> attempto mailing list
> attempto at lists.ifi.uzh.ch
> https://lists.ifi.uzh.ch/listinfo/attempto
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20120413/a8f37fa3/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/a8f37fa3/attachment-0001.png>