Determining what logic set contains a specific statement: DL, FOL, Second-Order

Question

I'm working on an Ontology to represent information in Starcraft, and I am having trouble determining if the following general class axiom can be represented in DL. If not, I would like to know the minimum logical set needed to express it (FOL, Second-order, etc).

With this axiom I want to represent that a player controls a region if (1) there exists a unit in that region and (2) every unit in that region is owned by the player.

I have 3 roles:

A. controlsRegion(p,r) where p is a player and r is a region

B. isOwnedBy(u,p) where u is a unit and p is a player

C. isInRegion(u,r) where u is a unit and r is a region

controlsRegion(p,r) \equiv \exists u.isInRegion(u,r) \sqcap 
                           \forall u.isInRegion(u,r) \circ isOwnedBy(u,p) 

Not enough rep to post image, see formula here: http://postimg.org/image/wve0h9m1z/

u, p, and r are variables (which is why I don't believe this can be represented in DL)

Also, I'm not sure if the syntax I'm using is correct, please advise how to properly represent it.

Thank you, any feedback is appreciated!

Answer 1

You may not be able to model this in general with OWL DL but you could model the region controled by P.

:RegionControlledByP  a  owl:Class;
    rdfs:subClassOf  [
        a  owl:Restriction;
        owl:onProperty  [ owl:inverseOf  :isInRegion ];
        owl:someValuesFrom  :Unit
    ], [
        a  owl:Restriction;
        owl:onProperty  [ owl:inverseOf  :isInRegion ];
        owl:allValuesFrom  [
            a  owl:Restriction;
            owl:onProperty  :isOwnedBy;
            owl:hasValue  :p
        ]
    ];  owl:equivalentClass  [
        a  owl:Restriction;
        owl:onProperty  [ owl:inverseOf  :controlsRegion ];
        owl:hasValue  :p
    ] .

If the players are all known, you can define such a class for each player. The more general case is maybe expressible in OWL Full but if it is, it involves complicated and non-standard use of the OWL vocabulary, that I'm afraid no reasoners can deal with completely.

Answer 2

Depending on the way that you represent the rest of the game, I think you can actually represent this in OWL DL, at least on a player by player basis. For instance, you can say that

=controlsRegion^-1.player ⊑ ∀(inRegion^-1 • ownedBy).{player}

In first order logic, that would be:

∀ r.[controlsRegion(player,r) ⇔ ∀ p' [(inRegion^-1•ownedBy)(r,p') ⇒ player = p']]

This says that the regions controlled by player are a subset of those all of whose regions are owned by player one. Of course, this means that you'd need to be able t infer that everything in a region can only be owned by player. That might be a bit of a challenge in OWL, which makes the Open World Assumption. It may require some work to be able to prove that there cannot be any things in a region that could be owned by someone else. This also only gives you the expression for one player at a time. You'd still need one such axiom for each player.