[Attempto] (How?) Can attempto describe these concepts?

[Norbert E. Fuchs]

On 27 Mar 2012, at 1:08 , Theodore H. Smith wrote:

> 
> On 26 Mar 2012, at 21:13, Norbert E. Fuchs wrote:
> 
>> 
>> The anaphor "its hands" is resolved to "hands of the car" which is not meant. Use instead
>> 
>> If a person drives a car then the person must have his/her own hands on the car's n:steering-wheel.
>> 
> 
> Thanks a lot Norbert. I'm starting to get more of a feel for attempto's language now.
> 
> I tried a basic "query", and I didn't get the answer I expected. Using http://attempto.ifi.uzh.ch/race/
> 
> If a person drives a car then the person must have his/her own hands on the car's n:steering-wheel.
> 	p:Fred is a person.
> 	p:Mary is a person.
> 	Mary drives a car.
> 
> And this theorem:
> 
> 	Mary has her own hands on a steering-wheel.
> 
> I get this "Theorems do not follow from axioms."
> 
> ( I asked a question before, and asked it off-list by accident, but that previous question had incorrect input, as I missed the "mary drives a car" statement. I fixed the input a bit. Hopefully there's no more glaring errors.)
> 
> Thanks all.

Theodore

I rephrased your first axiom to 

  If somebody X is a person and drives a car then X must have its own hands on the car's n:steering-wheel. 

and then got the following proof



Your original formulation of the first axiom 

  If a person drives a car then the person must have his/her own hands on the car's n:steering-wheel.

doesn't work currently since one of RACE's internal auxiliary axioms has a bug that I need to investigate.

Regards.

   --- nef
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20120329/0acda076/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2012-03-29 at 21.32.14 .png
Type: image/png
Size: 56025 bytes
Desc: not available
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20120329/0acda076/attachment-0001.png>