No inference when using "one of" and functional properties.

[wrobell]

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

1. House class.
2. House instances: house1, house2, house3, house4 and house5.
3. is next to property. It is symmetric and irreflexive.
4. is left to and is right to properties, which are inverse to each other and are sub-properties of is next to. They also are functional and inverse functional.
5. There is relationship between houses: house1 is left of house2, house2 is left of house3 and so on.

The problem is as follows

1. Define another house some house.
2. 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))

[Evgeny Blokhin]

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 avoids left_to and next_to, which might be here the key point.

[Dmitry Tsarkov]

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)

[wrobell]

To clarify the problem I would like to add

1. A house can be only one of house1, ..., house5.
2. some house is a house because domain of is next to is a house.
3. some house is not house1 - a house cannot be next to itself.
4. some house is not house3, house4, house5 - all these houses are not next to house1.
5. 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.

[Dmitry Tsarkov]

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?

[wrobell]

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.

[Dmitry Tsarkov]

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)
)

[Dmitry Tsarkov]

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.

[wrobell]

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.