[Attempto] Should I expect RACE to figure this out?

[Norbert E. Fuchs]

On 28 Mar 2012, at 20:10 , Joshua TAYLOR wrote:

> I tried running the axioms through the consistency checker, and got
> warnings "the room" (that if it was supposed to be anaphoric, then it
> needed a  referent).  I tried adding the axiom "There is a room." and
> the proof works:
> 
> Axioms: There is a room. A person is outside the room, or kicks a dog.
> The person is inside the room. if a person is outside the room then
> the person is not inside the room. if a person is inside the room then
> the person is not outside the room.
> 
> Theorems: A person kicks a dog.
> 
> Parameters:
> 
> The following minimal subsets of the axioms entail the theorems:
> 
>    Subset 1
> 
>        2: A person is outside the room, or kicks a dog.
>        3: The person is inside the room.
>        4: If a person is outside the room then the person is not
> inside the room.
> 
>    Subset 2
> 
>        2: A person is outside the room, or kicks a dog.
>        3: The person is inside the room.
>        5: If a person is inside the room then the person is not
> outside the room.
> 
> //JT
> 
> 
> On Wed, Mar 28, 2012 at 1:57 PM, Theodore H. Smith <delete at elfdata.com> wrote:
>> I have this input for RACE.
>> 
>> Axioms: A person is outside the room, or kicks a dog. The person is inside the room. if a person is outside the room then the person is not inside the room. if a person is inside the room then the person is not outside the room.
>> 
>> Theorems: a person kicks a dog.
>> 
>> Basically, in "Uncontrolled English", a person will kick the dog if he is inside the room. And he is inside the room. So he kicks the dog.
>> 
>> RACE doesn't figure this out. Is the problem with this line?: "A person is outside the room, or kicks a dog."
>> 
>> Is my input wrong? Or maybe RACE trips over that line?

Two clarifications.

First, Joshua writes

> I tried running the axioms through the consistency checker, and got
> warnings "the room" (that if it was supposed to be anaphoric, then it
> needed a  referent).  I tried adding the axiom "There is a room." and
> the proof works:

We need to distinguish between the warning of the ACE parser that "the room" has no antecedent, and RACE not being able to do the proof because the axioms do not introduce a room.

Second, as Kaarel wrote the axiom "If a person is outside a room then the person is not inside a room." is sufficient. You need not write "if a person is outside the room then the person is not inside the room. if a person is inside the room then the person is not outside the room."

Regards.
  
   --- nef