No inference when using "one of" and functional properties.
There is a possible bug when inferring with FaCT++. This bug report is based on the zebra puzzle for which a solution using OWL is presented here
http://folk.uio.no/martige/what/20120422/zebra.html
The solution defines
- House class.
- House instances: house1, house2, house3, house4 and house5.
is next to
property. It is symmetric and irreflexive.is left to
andis right to
properties, which are inverse to each other and are sub-properties ofis next to
. They also are functional and inverse functional.- There is relationship between houses: house1 is left of house2, house2 is left of house3 and so on.
The problem is as follows
- Define another house
some house
. - State that
some house
is next to house1.
Now, if we check if some house
is house2, FaCT++ says no. I would expect it to say yes, because there is only one house next to house1, the house2.
To illustrate the problem, I have implemented the example below. It is implemented using my Python bindings (https://bitbucket.org/wrobell/factplusplus/src/factpp/factpp/?at=factpp, sorry for no C++ version, please treat this as pseudocode)
import factpp
reasoner = factpp.Reasoner()
h1 = reasoner.individual('house1')
h2 = reasoner.individual('house2')
h3 = reasoner.individual('house3')
h4 = reasoner.individual('house4')
h5 = reasoner.individual('house5')
reasoner.different_individuals([h1, h2, h3, h4, h5])
house = reasoner.concept('House')
a_house = reasoner.one_of([h1, h2, h3, h4, h5])
reasoner.equal_concepts([house, a_house])
is_next_to = reasoner.object_role('is_next_to')
reasoner.set_symmetric(is_next_to)
reasoner.set_irreflexive(is_next_to)
reasoner.set_o_domain(is_next_to, house)
reasoner.set_o_range(is_next_to, house)
is_left_to = reasoner.object_role('is_left_to')
reasoner.implies_o_roles(is_left_to, is_next_to)
is_right_to = reasoner.inverse(is_left_to)
reasoner.implies_o_roles(is_right_to, is_next_to)
reasoner.set_o_functional(is_right_to)
reasoner.set_inverse_functional(is_right_to)
a_house_next = reasoner.max_o_cardinality(2, is_next_to, house)
reasoner.implies_concepts(house, a_house_next)
reasoner.related_to(h1, is_left_to, h2)
reasoner.related_to(h2, is_left_to, h3)
reasoner.related_to(h3, is_left_to, h4)
reasoner.related_to(h4, is_left_to, h5)
reasoner.related_to_not(h1, is_next_to, h5)
some_house = reasoner.individual('some house')
reasoner.related_to(some_house, is_next_to, h1)
assert reasoner.is_consistent()
print('some house is house 2:', reasoner.is_same_individuals(some_house, h2))
Comments (8)
-
-
repo owner Indeed, I remember that the Denis Ponomarev's variant was solved without problems. I'll have a look when I'll have more time (hopefully later this week)
-
reporter To clarify the problem I would like to add
- A house can be only one of house1, ..., house5.
some house
is a house because domain ofis next to
is a house.some house
is not house1 - a house cannot be next to itself.some house
is not house3, house4, house5 - all these houses are not next to house1.- Therefore
some house
can be house2 only.
Is any of above statements incorrect when considering FaCT++ reasoning algorithms?
BTW. If I explicitly state that
reasoner.different_individuals([some_house, h5]
then FaCT++ says that indeed
some house
is house2. -
repo owner The description seems correct and it should infer the house 2. From you btw comment is seems that related_to_not is not working as expected. Could you probably make a smaller test that confirms that guess?
-
reporter Any suggestions on how such test should look like?
One more discovery. If I add to the program in my first comment
reasoner.related_to_not(some_house, is_next_to, h5)
or
reasoner.related_to_not(h1, is_next_to, h4)
then the ontology becomes inconsistent.
-
repo owner I've tried to make the OWL ontology corresponding to your program as close as possible, and then test it in Protege. It works as expected (i.e., DLQuery tab shows that only h2 is the match for the some_house). Here is the ontology:
Prefix(:=<http://www.semanticweb.org/dmitrytsarkov/ontologies/2017/10/untitled-ontology-55#>) Prefix(owl:=<http://www.w3.org/2002/07/owl#>) Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>) Prefix(xml:=<http://www.w3.org/XML/1998/namespace>) Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>) Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>) Ontology(<http://www.semanticweb.org/dmitrytsarkov/ontologies/2017/10/untitled-ontology-55> Declaration(Class(:House)) Declaration(ObjectProperty(:is_left_to)) Declaration(ObjectProperty(:is_next_to)) Declaration(ObjectProperty(:is_right_to)) Declaration(NamedIndividual(:h1)) Declaration(NamedIndividual(:h2)) Declaration(NamedIndividual(:h3)) Declaration(NamedIndividual(:h4)) Declaration(NamedIndividual(:h5)) Declaration(NamedIndividual(:some_house)) ############################ # Object Properties ############################ # Object Property: :is_left_to (:is_left_to) SubObjectPropertyOf(:is_left_to :is_next_to) InverseObjectProperties(:is_left_to :is_right_to) # Object Property: :is_next_to (:is_next_to) SymmetricObjectProperty(:is_next_to) IrreflexiveObjectProperty(:is_next_to) ObjectPropertyDomain(:is_next_to :House) ObjectPropertyRange(:is_next_to :House) # Object Property: :is_right_to (:is_right_to) SubObjectPropertyOf(:is_right_to :is_next_to) FunctionalObjectProperty(:is_right_to) InverseFunctionalObjectProperty(:is_right_to) ############################ # Classes ############################ # Class: :House (:House) EquivalentClasses(:House ObjectOneOf(:h1 :h2 :h3 :h4 :h5)) SubClassOf(:House ObjectMaxCardinality(2 :is_next_to)) ############################ # Named Individuals ############################ # Individual: :h1 (:h1) ClassAssertion(:House :h1) ObjectPropertyAssertion(:is_left_to :h1 :h2) NegativeObjectPropertyAssertion(:is_next_to :h1 :h5) # Individual: :h2 (:h2) ClassAssertion(:House :h2) ObjectPropertyAssertion(:is_left_to :h2 :h3) # Individual: :h3 (:h3) ClassAssertion(:House :h3) ObjectPropertyAssertion(:is_left_to :h3 :h4) # Individual: :h4 (:h4) ClassAssertion(:House :h4) ObjectPropertyAssertion(:is_left_to :h4 :h5) # Individual: :h5 (:h5) ClassAssertion(:House :h5) # Individual: :some_house (:some_house) ClassAssertion(:House :some_house) ObjectPropertyAssertion(:is_next_to :some_house :h1) DifferentIndividuals(:h1 :h2 :h3 :h4 :h5) )
-
repo owner In order to find our where exactly the problem lies, you can try to simplify your original test case in all possible ways, and see whether the error still present: - leave only 3 houses; - remove unnecessary roles (definitely is_right_to, probably is_left_to)
Additionally you can try to produce a C++ testcase that use just FaCT++ calls.
-
reporter - changed status to invalid
Thanks for the example. It was my own mistake in my Python bindings causing the issue. I will try to confirm any problem with C++ example next time. Sorry for wasting your time.
- Log in to comment
It should be noted that Denis Ponomaryov in his zebra puzzle implementation from here:
http://persons.iis.nsk.su/en/person/ponom/ontologies/
uses the only
owl:InverseFunctionalProperty
right_to
and avoidsleft_to
andnext_to
, which might be here the key point.