确定哪个逻辑集包含特定语句:DL、FOL、Second Order

Question

我正在研究一个本体论来表示星际争霸中的信息，我很难确定以下通用类公理是否可以在DL中表示。如果不是，我想知道表达它所需的最小逻辑集（FOL、二阶等）。

有了这个公理，我想表示玩家控制一个区域，如果（1）该区域中存在一个单位，并且（2）该区域的每个单位都归玩家所有

我有三个角色：

A。controlsRegion（p，r），其中p是玩家，r是区域

B。isOwnedBy（u，p）其中u是一个单位，p是一个玩家

C。isInRegion（u，r），其中u是单位，r是区域

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

没有足够的代表发布图片，请参阅此处的公式：http://postimg.org/image/wve0h9m1z/

u、 p和r是变量（这就是为什么我不相信这可以在DL中表示）

此外，我不确定我使用的语法是否正确，请建议如何正确地表示它。

谢谢，任何反馈都将不胜感激！

Answer 1

您可能无法用OWL DL对其进行一般建模，但您可以对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
    ] .

如果玩家都是已知的，你可以为每个玩家定义这样一个类。更普遍的情况可能可以用OWL-Full表达，但如果是这样的话，它涉及到OWL词汇的复杂和非标准的使用，恐怕没有推理者能够完全处理这些问题。

Answer 2

根据您表示游戏其余部分的方式，我认为您实际上可以在OWL DL中表示这一点，至少在逐个玩家的基础上是这样。例如，你可以说

=controlsRegion^-1.player&sqsubsteq&forall；（在Region^-1&bullet；ownedBy中）。｛玩家｝

在一阶逻辑中，这将是：

∀r.[controlsRegion（player，r）&iff；∀p'[（inRegion^-1&bullet；ownedBy）（r，p'）&Rightarrow；player=p']]

这意味着玩家控制的区域是所有区域都归玩家一所有的区域的子集。当然，这意味着你需要能够推断出一个区域中的所有都只能由玩家拥有。这可能是OWL的一个挑战，它提出了开放世界假设。这可能需要一些工作才能证明在一个地区不可能有任何东西被其他人拥有。这也只为一次提供一个玩家的表达式。每个玩家仍然需要一条这样的公理。