Materialized Reasoner | AllegroGraph 8.4.0 (original) (raw)

eq-ref

T(?s, ?p, ?o)

T(?s, owl:sameAs, ?s)
T(?p, owl:sameAs, ?p)
T(?o, owl:sameAs, ?o)

eq-sym

11 same-as

T(?x, owl:sameAs, ?y)

T(?y, owl:sameAs, ?x)

eq-trans

11 same-as

T(?x, owl:sameAs, ?y)
T(?y, owl:sameAs, ?z)

T(?x, owl:sameAs, ?z)

eq-rep-s

11 same-as

T(?s, owl:sameAs, ?s')
T(?s, ?p, ?o)

T(?s', ?p, ?o)

eq-rep-p

11 same-as

T(?p, owl:sameAs, ?p')
T(?s, ?p, ?o)

T(?s, ?p', ?o)

eq-rep-o

11 same-as

T(?o, owl:sameAs, ?o')
T(?s, ?p, ?o)

T(?s, ?p, ?o')

eq-diff1

T(?x, owl:sameAs, ?y)
T(?x, owl:differentFrom, ?y)

inconsistent

eq-diff2

T(?x, rdf:type, owl:AllDifferent)
T(?x, owl:members, ?y)
LIST[?y, ?z1, ..., ?zn]
T(?zi, owl:sameAs, ?zj)

inconsistent

for each 1 ≤ i < j ≤ n

eq-diff3

T(?x, rdf:type, owl:AllDifferent)
T(?x, owl:distinctMembers, ?y)
LIST[?y, ?z1, ..., ?zn]
T(?zi, owl:sameAs, ?zj)

inconsistent

for each 1 ≤ i < j ≤ n

prp-ap

T(ap, rdf:type, owl:AnnotationProperty)

for each built-in annotation property of OWL 2 RL

prp-dom

T(?p, rdfs:domain, ?c)
T(?x, ?p, ?y)

T(?x, rdf:type, ?c)

prp-rng

T(?p, rdfs:range, ?c)
T(?x, ?p, ?y)

T(?y, rdf:type, ?c)

prp-fp

T(?p, rdf:type, owl:FunctionalProperty)
T(?x, ?p, ?y1)
T(?x, ?p, ?y2)

T(?y1, owl:sameAs, ?y2)

prp-ifp

T(?p, rdf:type, owl:InverseFunctionalProperty)
T(?x1, ?p, ?y)
T(?x2, ?p, ?y)

T(?x1, owl:sameAs, ?x2)

prp-irp

T(?p, rdf:type, owl:IrreflexiveProperty)
T(?x, ?p, ?x)

inconsistent

prp-symp

T(?p, rdf:type, owl:SymmetricProperty)
T(?x, ?p, ?y)

T(?y, ?p, ?x)

prp-asyp

T(?p, rdf:type, owl:AsymmetricProperty)
T(?x, ?p, ?y)
T(?y, ?p, ?x)

inconsistent

prp-trp

T(?p, rdf:type, owl:TransitiveProperty)
T(?x, ?p, ?y)
T(?y, ?p, ?z)

T(?x, ?p, ?z)

prp-spo1

T(?p1, rdfs:subPropertyOf, ?p2)
T(?x, ?p1, ?y)

T(?x, ?p2, ?y)

prp-spo2

T(?p, owl:propertyChainAxiom, ?x)
LIST[?x, ?p1, ..., ?pn]
T(?u1, ?p1, ?u2)
T(?u2, ?p2, ?u3)
...
T(?un, ?pn, ?un+1)

T(?u1, ?p, ?un+1)

prp-eqp1

T(?p1, owl:equivalentProperty, ?p2)
T(?x, ?p1, ?y)

T(?x, ?p2, ?y)

prp-eqp2

T(?p1, owl:equivalentProperty, ?p2)
T(?x, ?p2, ?y)

T(?x, ?p1, ?y)

prp-pdw

T(?p1, owl:propertyDisjointWith, ?p2)
T(?x, ?p1, ?y)
T(?x, ?p2, ?y)

inconsistent

prp-adp

T(?x, rdf:type, owl:AllDisjointProperties)
T(?x, owl:members, ?y)
LIST[?y, ?p1, ..., ?pn]
T(?u, ?pi, ?v)
T(?u, ?pj, ?v)

inconsistent

for each 1 ≤ i < j ≤ n

prp-inv1

T(?p1, owl:inverseOf, ?p2)
T(?x, ?p1, ?y)

T(?y, ?p2, ?x)

prp-inv2

T(?p1, owl:inverseOf, ?p2)
T(?x, ?p2, ?y)

T(?y, ?p1, ?x)

prp-key

T(?c, owl:hasKey, ?u)
LIST[?u, ?p1, ..., ?pn]
T(?x, rdf:type, ?c)
T(?x, ?p1, ?z1)
...
T(?x, ?pn, ?zn)
T(?y, rdf:type, ?c)
T(?y, ?p1, ?z1)
...
T(?y, ?pn, ?zn)

T(?x, owl:sameAs, ?y)

prp-npa1

T(?x, owl:sourceIndividual, ?i1)
T(?x, owl:assertionProperty, ?p)
T(?x, owl:targetIndividual, ?i2)
T(?i1, ?p, ?i2)

inconsistent

prp-npa2

T(?x, owl:sourceIndividual, ?i)
T(?x, owl:assertionProperty, ?p)
T(?x, owl:targetValue, ?lt)
T(?i, ?p, ?lt)

inconsistent

cls-thing

T(owl:Thing, rdf:type, owl:Class)

cls-nothing1

T(owl:Nothing, rdf:type, owl:Class)

cls-nothing2

T(?x, rdf:type, owl:Nothing)

inconsistent

cls-int1

11 class

T(?c, owl:intersectionOf, ?x)
LIST[?x, ?c1, ..., ?cn]
T(?y, rdf:type, ?c1)
T(?y, rdf:type, ?c2)
...
T(?y, rdf:type, ?cn)

T(?y, rdf:type, ?c)

cls-int2

11 class

T(?c, owl:intersectionOf, ?x)
LIST[?x, ?c1, ..., ?cn]
T(?y, rdf:type, ?c)

T(?y, rdf:type, ?c1)
T(?y, rdf:type, ?c2)
...
T(?y, rdf:type, ?cn)

cls-uni

11 class

T(?c, owl:unionOf, ?x)
LIST[?x, ?c1, ..., ?cn]
T(?y, rdf:type, ?ci)

T(?y, rdf:type, ?c)

for each 1 ≤ i ≤ n

cls-com

T(?c1, owl:complementOf, ?c2)
T(?x, rdf:type, ?c1)
T(?x, rdf:type, ?c2)

inconsistent

cls-svf1

11 restriction & values-from

T(?x, owl:someValuesFrom, ?y)
T(?x, owl:onProperty, ?p)
T(?u, ?p, ?v)
T(?v, rdf:type, ?y)

T(?u, rdf:type, ?x)

cls-svf2

11 restriction & values-from

T(?x, owl:someValuesFrom, owl:Thing)
T(?x, owl:onProperty, ?p)
T(?u, ?p, ?v)

T(?u, rdf:type, ?x)

cls-avf

11 restriction & values-from

T(?x, owl:allValuesFrom, ?y)
T(?x, owl:onProperty, ?p)
T(?u, rdf:type, ?x)
T(?u, ?p, ?v)

T(?v, rdf:type, ?y)

cls-hv1

11 restriction & values-from

T(?x, owl:hasValue, ?y)
T(?x, owl:onProperty, ?p)
T(?u, rdf:type, ?x)

T(?u, ?p, ?y)

cls-hv2

11 restriction & values-from

T(?x, owl:hasValue, ?y)
T(?x, owl:onProperty, ?p)
T(?u, ?p, ?y)

T(?u, rdf:type, ?x)

cls-maxc1

T(?x, owl:maxCardinality, "0"^^xsd:nonNegativeInteger)
T(?x, owl:onProperty, ?p)
T(?u, rdf:type, ?x)
T(?u, ?p, ?y)

inconsistent

cls-maxc2

11 restriction

T(?x, owl:maxCardinality, "1"^^xsd:nonNegativeInteger)
T(?x, owl:onProperty, ?p)
T(?u, rdf:type, ?x)
T(?u, ?p, ?y1)
T(?u, ?p, ?y2)

T(?y1, owl:sameAs, ?y2)

cls-maxqc1

T(?x, owl:maxQualifiedCardinality, "0"^^xsd:nonNegativeInteger)
T(?x, owl:onProperty, ?p)
T(?x, owl:onClass, ?c)
T(?u, rdf:type, ?x)
T(?u, ?p, ?y)
T(?y, rdf:type, ?c)

inconsistent

cls-maxqc2

T(?x, owl:maxQualifiedCardinality, "0"^^xsd:nonNegativeInteger)
T(?x, owl:onProperty, ?p)
T(?x, owl:onClass, owl:Thing)
T(?u, rdf:type, ?x)
T(?u, ?p, ?y)

inconsistent

cls-maxqc3

11 restriction

T(?x, owl:maxQualifiedCardinality, "1"^^xsd:nonNegativeInteger)
T(?x, owl:onProperty, ?p)
T(?x, owl:onClass, ?c)
T(?u, rdf:type, ?x)
T(?u, ?p, ?y1)
T(?y1, rdf:type, ?c)
T(?u, ?p, ?y2)
T(?y2, rdf:type, ?c)

T(?y1, owl:sameAs, ?y2)

cls-maxqc4

11 restriction

T(?x, owl:maxQualifiedCardinality, "1"^^xsd:nonNegativeInteger)
T(?x, owl:onProperty, ?p)
T(?x, owl:onClass, owl:Thing)
T(?u, rdf:type, ?x)
T(?u, ?p, ?y1)
T(?u, ?p, ?y2)

T(?y1, owl:sameAs, ?y2)

cls-oo

T(?c, owl:oneOf, ?x)
LIST[?x, ?y1, ..., ?yn]

T(?y1, rdf:type, ?c)
...
T(?yn, rdf:type, ?c)

cax-sco

T(?c1, rdfs:subClassOf, ?c2)
T(?x, rdf:type, ?c1)

T(?x, rdf:type, ?c2)

cax-eqc1

11 class

T(?c1, owl:equivalentClass, ?c2)
T(?x, rdf:type, ?c1)

T(?x, rdf:type, ?c2)

cax-eqc2

11 class

T(?c1, owl:equivalentClass, ?c2)
T(?x, rdf:type, ?c2)

T(?x, rdf:type, ?c1)

cax-dw

T(?c1, owl:disjointWith, ?c2)
T(?x, rdf:type, ?c1)
T(?x, rdf:type, ?c2)

inconsistent

cax-adc

T(?x, rdf:type, owl:AllDisjointClasses)
T(?x, owl:members, ?y)
LIST[?y, ?c1, ..., ?cn]
T(?z, rdf:type, ?ci)
T(?z, rdf:type, ?cj)

inconsistent

for each 1 ≤ i < j ≤ n

dt-type1

T(dt, rdf:type, rdfs:Datatype)

for each datatype dt supported in OWL 2 RL

dt-type2

T(lt, rdf:type, dt)

for each literal lt and each datatype dt supported in OWL 2 RL such that the data value of lt is contained in the value space of dt

dt-eq

T(lt1, owl:sameAs, lt2)

for all literals lt1 and lt2 with the same data value

dt-diff

T(lt1, owl:differentFrom, lt2)

for all literals lt1 and lt2 with different data values

dt-not-type

T(lt, rdf:type, dt)

inconsistent

for each literal lt and each datatype dt supported in OWL 2 RL
such that t

scm-cls

11 class

T(?c, rdf:type, owl:Class)

T(?c, rdfs:subClassOf, ?c)
T(?c, owl:equivalentClass, ?c)
T(?c, rdfs:subClassOf, owl:Thing)
T(owl:Nothing, rdfs:subClassOf, ?c)

scm-sco

11 always

T(?c1, rdfs:subClassOf, ?c2)
T(?c2, rdfs:subClassOf, ?c3)

T(?c1, rdfs:subClassOf, ?c3)

scm-eqc1

T(?c1, owl:equivalentClass, ?c2)

T(?c1, rdfs:subClassOf, ?c2)
T(?c2, rdfs:subClassOf, ?c1)

scm-eqc2

T(?c1, rdfs:subClassOf, ?c2)
T(?c2, rdfs:subClassOf, ?c1)

T(?c1, owl:equivalentClass, ?c2)

scm-op

T(?p, rdf:type, owl:ObjectProperty)

T(?p, rdfs:subPropertyOf, ?p)
T(?p, owl:equivalentProperty, ?p)

scm-dp

T(?p, rdf:type, owl:DatatypeProperty)

T(?p, rdfs:subPropertyOf, ?p)
T(?p, owl:equivalentProperty, ?p)

scm-spo

T(?p1, rdfs:subPropertyOf, ?p2)
T(?p2, rdfs:subPropertyOf, ?p3)

T(?p1, rdfs:subPropertyOf, ?p3)

scm-eqp1

T(?p1, owl:equivalentProperty, ?p2)

T(?p1, rdfs:subPropertyOf, ?p2)
T(?p2, rdfs:subPropertyOf, ?p1)

scm-eqp2

T(?p1, rdfs:subPropertyOf, ?p2)
T(?p2, rdfs:subPropertyOf, ?p1)

T(?p1, owl:equivalentProperty, ?p2)

scm-dom1

T(?p, rdfs:domain, ?c1)
T(?c1, rdfs:subClassOf, ?c2)

T(?p, rdfs:domain, ?c2)

scm-dom2

T(?p2, rdfs:domain, ?c)
T(?p1, rdfs:subPropertyOf, ?p2)

T(?p1, rdfs:domain, ?c)

scm-rng1

T(?p, rdfs:range, ?c1)
T(?c1, rdfs:subClassOf, ?c2)

T(?p, rdfs:range, ?c2)

scm-rng2

T(?p2, rdfs:range, ?c)
T(?p1, rdfs:subPropertyOf, ?p2)

T(?p1, rdfs:range, ?c)

scm-hv

T(?c1, owl:hasValue, ?i)
T(?c1, owl:onProperty, ?p1)
T(?c2, owl:hasValue, ?i)
T(?c2, owl:onProperty, ?p2)
T(?p1, rdfs:subPropertyOf, ?p2)

T(?c1, rdfs:subClassOf, ?c2)

scm-svf1

T(?c1, owl:someValuesFrom, ?y1)
T(?c1, owl:onProperty, ?p)
T(?c2, owl:someValuesFrom, ?y2)
T(?c2, owl:onProperty, ?p)
T(?y1, rdfs:subClassOf, ?y2)

T(?c1, rdfs:subClassOf, ?c2)

scm-svf2

T(?c1, owl:someValuesFrom, ?y)
T(?c1, owl:onProperty, ?p1)
T(?c2, owl:someValuesFrom, ?y)
T(?c2, owl:onProperty, ?p2)
T(?p1, rdfs:subPropertyOf, ?p2)

T(?c1, rdfs:subClassOf, ?c2)

scm-avf1

T(?c1, owl:allValuesFrom, ?y1)
T(?c1, owl:onProperty, ?p)
T(?c2, owl:allValuesFrom, ?y2)
T(?c2, owl:onProperty, ?p)
T(?y1, rdfs:subClassOf, ?y2)

T(?c1, rdfs:subClassOf, ?c2)

scm-avf2

T(?c1, owl:allValuesFrom, ?y)
T(?c1, owl:onProperty, ?p1)
T(?c2, owl:allValuesFrom, ?y)
T(?c2, owl:onProperty, ?p2)
T(?p1, rdfs:subPropertyOf, ?p2)

T(?c2, rdfs:subClassOf, ?c1)

scm-int

T(?c, owl:intersectionOf, ?x)
LIST[?x, ?c1, ..., ?cn]

T(?c, rdfs:subClassOf, ?c1)
T(?c, rdfs:subClassOf, ?c2)
...
T(?c, rdfs:subClassOf, ?cn)

scm-uni

T(?c, owl:unionOf, ?x)
LIST[?x, ?c1, ..., ?cn]

T(?c1, rdfs:subClassOf, ?c)
T(?c2, rdfs:subClassOf, ?c)
...
T(?cn, rdfs:subClassOf, ?c)