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

[Norbert E. Fuchs]

David

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

> Researching further, RACE does seem to do queries that include negation:
> Axioms: Every man is a human. Every woman is a human. Mary is a woman. John is a man. Fido is a dog. No dog is a human.
> 
> Query: Who is not a human?
> 
> Parameters:
> 
> The following minimal subsets of the axioms answer the query:
> 
> Subset 1
> 	• 5: Fido is a dog.
> 	• 6: No dog is a human.
> 	• Substitution: who = (at least 1) dog

This answer is correct. Where is the problem?

> Maybe the problem is "and" processing. I get the same result from this query:
> Axioms: Every man is a human. Every woman is a human. Mary is a woman. John is a man. Fido is a dog. No dog is a human.
> 
> Query: Who is a man and is a woman ?
> 
> Parameters:
> 
> Query cannot be answered

This answer is correct, since there is no individual that is both a man and a woman. Again the text should be changed to "Query does not follow from axioms."

> Also: this is the full cut-and-paste for the woman who is not human:
> 
> Axioms: Every man is a human. Every woman is a human. Mary is a woman. John is a man.
> 
> Query: Who is a woman and is not a human?
> 
> Parameters:
> 
> Query cannot be answered.

See above.

> I was experimenting with RACE, and don't understand the results I get below, specifically Subset 3 and Subset 6
> I can understand that "something" is acting as a name for a constant but when Something = Mary how do I express
> the idea that the substitution is under the constraint of being male ?
> 
> Axioms: Every man is a human. Every woman is a human. Mary is a woman. John is a man. Fido is a dog. No dog is a human. John is a male. Fido is a male.
> 
> Theorems: Something is a male.
> 
> Parameters:
> 
> The following minimal subsets of the axioms entail the theorems:
> 
> 	• Subset 1
> 		• 7: John is a male.
> 		• Substitution: something = Fido
> 	• Subset 2
> 		• 7: John is a male.
> 		• Substitution: something = John
> 	• Subset 3
> 		• 7: John is a male.
> 		• Substitution: something = Mary
> 	• Subset 4
> 		• 8: Fido is a male.
> 		• Substitution: something = Fido
> 	• Subset 5
> 		• 8: Fido is a male.
> 		• Substitution: something = John
> 	• Subset 6
> 		• 8: Fido is a male.
> 		• Substitution: something = Mary

This is a bug – variables were not unified correctly – that I corrected in the meantime. Thanks for finding it. Now you get the correct answer

The following minimal subsets of the axioms entail the theorems:

	• Subset 1
		• 7: John is a male.
		• Substitution: something = John
	• Subset 2
		• 8: Fido is a male.
		• Substitution: something = Fido

Regards.

   --- nef