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

[Joshua TAYLOR]

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?
> _______________________________________________
> attempto mailing list
> attempto at lists.ifi.uzh.ch
> https://lists.ifi.uzh.ch/listinfo/attempto



-- 
Joshua Taylor, http://www.cs.rpi.edu/~tayloj/