complexity of reasoning in DAML-ONT

Theorem:

Determining consistency in DAML-ONT 1.2 is NP-hard in terms of data
complexity, where we say that the schema/rule base is the class definitions
and the data consists of statements about the type of objects and
statements about the relationships between objects.

Proof:

The proof is by reduction from 3CNF satisfiability.  

Let C = (l11 v ... v l13) ^ ... ^ ( ln v ... v ln3 ) be a propositional
formula in 3CNF form, with variables v1, ..., vk,
where each lij is of the form vh or -vh for some 1<=h<=k.

The schema will be 

<Property ID="complement"/>
<Property ID="disjunct"/>

<Class ID="LiteralTrue">
  <restrictedBy>
    <Restriction>
      <onProperty resource="#complement"/>
      <toClass resource="#LiteralFalse"/>
    </Restriction>
  </restrictedBy>
</Class>

<Class ID="LiteralFalse">
  <restrictedBy>
    <Restriction>
      <onProperty resource="#complement"/>
      <toClass resource="#LiteralTrue"/>
    </Restriction>
  </restrictedBy>
</Class>

<Class ID="Literal">
  <UnionOf>
    <Class about="LiteralTrue">
    <Class about="LiteralFalse">
  </UnionOf>
</Class>

<Class ID="SatisfiedClause">
  <qualifiedBy>
    <Qualification>
      <onProperty resource="#disjunct"/>
      <hasValue resource="#LiteralTrue"/>
    </Qualification>
  </qualifiedBy>
</Class>

The data will be

1/ for 1 <= i <= k

<Literal id="vipositive">  
  <complement about="#vinegative">
</Literal>
<Literal id="vinegative"/>  
  <complement about="#vipositive">
</Literal>

2/ for 1 <= i <= n

<SatisfiedClause id="ci">
  <disjunct about=eli1>
  <disjunct about=eli2>
  <disjunct about=eli3>
</Clause>

where elij is "#vhpositive" if lij is vh
          and "#vhnegative" if lij is -vh

So each variable gives rise to two objects, a positive and a negative
literal.  Now these two objects are both in the class Literal, which is
the union of LiteralTrue and LiteralFalse, and they are related to each
other by the complement property.  Therefore one has to be in LiteralTrue
and the other in LiteralFalse.  This essentially forces an interpretation
on the variables.

Under this reading of the classes LiteralTrue and LiteralFalse, an object
belongs to SatisfiedClause if and only if the clause it represents is
satisfied in the interpretation.  Therefore the entire collection of
statements is consistent if and only if there is an interpretation that
simultaneously satisfies all the clauses, i.e., the formula is satisfiable.


Note that this example does not use equivalentTo, doesn't make any extra
statements about the union class Literal, and doesn't depend on any
possible-to-misunderstand meaning for any of the DAML-ONT constructs.  
The example would even work if Literal was interpreted as some subset of
the union of LiteralTrue and LiteralFalse.

Received on Monday, 16 October 2000 16:20:02 UTC