De Morgen rules for quantifiers

tests/test_reasoner_alc_father_ontology.py

@@ -1,5 +1,5 @@
 from owlapy.owl_reasoner import SyncReasoner
-from owlapy.class_expression import OWLClass, OWLObjectSomeValuesFrom
+from owlapy.class_expression import OWLClass, OWLObjectSomeValuesFrom, OWLObjectAllValuesFrom
 from owlapy.owl_individual import OWLNamedIndividual
 from owlapy.iri import IRI
 from owlapy.owl_property import OWLObjectProperty
@@ -23,28 +23,37 @@ def test_readme(self):
  # hasChild object property
  hasChild = OWLObjectProperty(IRI('http://example.com/father#', 'hasChild'))
 
- # Things
+ # Sanity checking = Things
  assert hermit.instances(thing) == {OWLNamedIndividual(IRI('http://example.com/father#', 'anna')), OWLNamedIndividual(IRI('http://example.com/father#', 'martin')), OWLNamedIndividual(IRI('http://example.com/father#', 'heinz')), OWLNamedIndividual(IRI('http://example.com/father#', 'stefan')), OWLNamedIndividual(IRI('http://example.com/father#', 'michelle')), OWLNamedIndividual(IRI('http://example.com/father#', 'markus'))}
-
  # De Morgen Rules : Thing \equiv \neg Bottom
  assert hermit.instances(thing) == hermit.instances(nothing.get_object_complement_of())
 
- # hasChild a thing.
+ # Sanity checking = \exist hasChild Thing.
  assert hermit.instances(OWLObjectSomeValuesFrom(property=hasChild, filler=thing)) == eval(
  "{OWLNamedIndividual(IRI('http://example.com/father#', 'markus')), OWLNamedIndividual(IRI('http://example.com/father#', 'martin')), OWLNamedIndividual(IRI('http://example.com/father#', 'stefan')), OWLNamedIndividual(IRI('http://example.com/father#', 'anna'))}")
-
- # hasChild a person.
+ # Sanity checking \exist hasChild Person.
  assert hermit.instances(OWLObjectSomeValuesFrom(property=hasChild, filler=person)) == eval(
  "{OWLNamedIndividual(IRI('http://example.com/father#', 'markus')), OWLNamedIndividual(IRI('http://example.com/father#', 'martin')), OWLNamedIndividual(IRI('http://example.com/father#', 'stefan')), OWLNamedIndividual(IRI('http://example.com/father#', 'anna'))}")
+ # \exist hasChild a person = \exist hasChild a thing
+ assert hermit.instances(OWLObjectSomeValuesFrom(property=hasChild, filler=thing)) == hermit.instances(
+ OWLObjectSomeValuesFrom(property=hasChild, filler=person))
 
- # hasChild a female.
+ # Sanity checking: \exist hasChild a female.
  assert hermit.instances(OWLObjectSomeValuesFrom(property=hasChild, filler=female)) == eval(
  "{OWLNamedIndividual(IRI('http://example.com/father#', 'markus'))}")
  # Question: hasChild something that hasChild a female.
- # Answer: stefan
- # (stefan haschild markus) and markus haschild anna
+ # Answer: stefan: (stefan haschild markus) and (markus haschild anna)
  assert hermit.instances(OWLObjectSomeValuesFrom(property=hasChild,
  filler=OWLObjectSomeValuesFrom(property=hasChild,
  filler=female))) == eval(
  "{OWLNamedIndividual(IRI('http://example.com/father#', 'stefan'))}")
-
+ # De morgen rule: \neg \exist r \neg T = \forall r T
+ c = thing
+ forall_r_c = OWLObjectAllValuesFrom(hasChild, c)
+ neg_exist_r_neg_c = OWLObjectSomeValuesFrom(hasChild, c.get_object_complement_of()).get_object_complement_of()
+ assert hermit.instances(neg_exist_r_neg_c) == hermit.instances(forall_r_c)
+ # De morgen rule: \neg \exist r \neg bottom = \forall r bottom
+ c = nothing
+ forall_r_c = OWLObjectAllValuesFrom(hasChild, c)
+ neg_exist_r_neg_c = OWLObjectSomeValuesFrom(hasChild, c.get_object_complement_of()).get_object_complement_of()
+ assert hermit.instances(neg_exist_r_neg_c) == hermit.instances(forall_r_c)