From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Mon, 16 Oct 2000 16:19:23 -0400

To: www-rdf-logic@w3.org

Message-Id: <20001016161923H.pfps@research.bell-labs.com>

Date: Mon, 16 Oct 2000 16:19:23 -0400

To: www-rdf-logic@w3.org

Message-Id: <20001016161923H.pfps@research.bell-labs.com>

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 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:52:37 GMT
*