[Attempto] Non-monotonic reasoning in RACE

[David Whitten]

Norbert,
thank you for the hard work on RACE.
I did use the interface at http://attempto.ifi.uzh.ch/race/
and got results that I expected:

*Axioms*: 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.

*Theorems*: Kelly is a woman.

*Parameters*:

Theorems do not follow from axioms.
overall time: 0.585 sec; RACE time: 0.024 sec

*Axioms*: 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.

*Theorems*: Kelly is a man.

*Parameters*:

The following minimal subsets of the axioms entail the theorems:
Subset 1

   - 5: Kelly is a human.
   - 6: If a human is not provably a woman then the human is a man.



On Mon, Aug 17, 2015 at 12:32 PM, Norbert E. Fuchs <fuchs at ifi.uzh.ch> wrote:

>
> On 11 Aug 2015, at 13:47 , David Whitten <whitten at netcom.com> wrote:
>
> I don't know what I have done wrong.
>
> 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.
>
> I had the axiom set:
>
> 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.
>
> I had the query:
>
> Who is a man and is a human?
>
> RACE said: overall time: 0.552 sec; RACE time: 0.04 sec
> 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.
>
> Query: Who is a man and is a human?
>
> Parameters:
>
> The following minimal subsets of the axioms answer the query:
>
> • Subset 1
> • 3: Mary is a human that is a woman.
> • 6: If a human is not provably a woman then the human is a man.
> • Substitution: who = (at least 1) woman
> • Subset 2
> • 3: Mary is a human that is a woman.
> • 6: If a human is not provably a woman then the human is a man.
> • Substitution: who = Mary
> • Subset 3
> • 4: John is a human that is a man.
> • Substitution: who = John
> • Subset 4
> • 5: Mack is a human.
> • 6: If a human is not provably a woman then the human is a man.
> • Substitution: who = Mack
>
>
> David
>
> I had suggested non-redundant axioms
>
>   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.
>
> 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.
>
>
>
>
> 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 ..."
>
>
> while the combination "... not ... not provable P ..." is not accepted as
> being semantically identically to "P".
>
>
> Any comments or suggestions?
>
> Best regards.
>
>    --- nef
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20150819/3066cf16/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2015-08-17 at 18.25.08 .png
Type: image/png
Size: 123804 bytes
Desc: not available
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20150819/3066cf16/attachment-0003.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2015-08-17 at 18.12.30 .png
Type: image/png
Size: 162664 bytes
Desc: not available
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20150819/3066cf16/attachment-0004.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2015-08-17 at 18.21.46 .png
Type: image/png
Size: 164058 bytes
Desc: not available
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20150819/3066cf16/attachment-0005.png>