[Pellet-users] still: missing solutions and some weird behavior
Wolfgang May
may at informatik.uni-goettingen.de
Thu Oct 25 16:37:49 UTC 2007
Hi,
(was: pellet.exceptions.InternalReasonerException XXX
is not in the definition order)
On Wed, 24 Oct 2007, Ibach, Brandon L wrote:
> I agree with Evren that there's nothing in the given ontology to support
> the equivalence of DrawNode2 and DrawNode, mainly because of the lack of
> support for the disjointedness of WinNode, LoseNode and
> DrawNode/DrawNode2.
Sorry, that was a misunderstanding (the main thing I wanted to say with
it that DrawNode2 is not a typo). The sample was a simplified fragment
of the whole thing that showed the error message. The original code
included owl11:DisjointUnionOf (Lose Draw Win), but I wanted not to
use owl11 for the question.
So far, I solved it by now, but still with some weird behavior (see below).
[...]
> It's an interesting exercise, in any case. Care to explain a bit more
> about the application driving the model?
It's a pebble "Win Move Game". This example is often used in Logic
programming as an example for well-founded/stable models:
There is a directed graph, and one pebble which is placed on a position.
Two players move the pebble through the graph alternately. When a player
cannot move, he loses.
-> A position is lost if (1) it has no exit, or (2) all exits go to
nodes that are won (for the other player).
Thus, the player who is on the move cannot move, or only to a node
where the other will win eventually ((1) is subsumed by (2)).
-> A position is won if there is an exit going to a LoseNode (because
the player who is on the move can move there and the other one loses)
-> other nodes are drawn (i.e. in a graph a->b->c->a, the game will
run forever).
-> For all positions, assuming that both players play optimally,
it can be checked whether the player who is on the move will lose or
win eventually, or if the game is drawn.
Thus with
:Node a owl:Class;
owl:equivalentClass [owl11:disjointUnionOf ( :WinNode :LoseNode :DrawNode )].
:DrawNode is defined as those nodes that are neither WinNodes or
LoseNodes.
The other characterizaton :DrawNode2 is equivalent, but more
"constructive".
*** Having this done, there is some weird behavior:
* four files in the attachment:
- winmove-axioms-draw.n3 (the axioms)
- winmove-graph.n3 (a sample graph)
- winmove-closure.n3 (closing the "edge" relation)
- winmove-drawnodes.sparql (test query)
running the winmove-drawnodes.sparql reading the three input N3s yields
the correct result:
****
prefix owl: <http://www.w3.org/2002/07/owl#>
prefix : <foo://bla/>
select ?C ?W ?L ?D ?D2
from <file:winmove-graph.n3>
from <file:winmove-axioms-draw.n3>
from <file:winmove-closure.n3>
where {{:DrawNode owl:equivalentClass ?C} UNION
{?W a :WinNode} UNION
{?D a :DrawNode} UNION
{?D2 a :DrawNode2} UNION
{?L a :LoseNode}}
Reading Model from File file:winmove-graph.n3
Reading Model from File file:winmove-axioms-draw.n3
Reading Model from File file:winmove-closure.n3
Building Model with inference support. Using Pellet-Plugin.
Query result as plain text:
-----------------------------------------------------------------------------------------
| C | W | L | D | D2 |
=========================================================================================
| <foo://bla/DrawNode2> | | | | |
| <foo://bla/DrawNode> | | | | |
| | <foo://bla/a> | | | |
| | <foo://bla/d> | | | |
| | <foo://bla/b> | | | |
| | <foo://bla/c> | | | |
| | <foo://bla/i> | | | |
| | | | <foo://bla/m> | |
| | | | <foo://bla/h> | |
| | | | <foo://bla/g> | |
| | | | | <foo://bla/m> |
| | | | | <foo://bla/h> |
| | | | | <foo://bla/g> |
| | | <foo://bla/k> | | |
| | | <foo://bla/j> | | |
| | | <foo://bla/f> | | |
| | | <foo://bla/e> | | |
| | | <foo://bla/l> | | |
-----------------------------------------------------------------------------------------
Successfully printed 18 query results.
Finished.
*****
When I uncomment the two lines about :m in the file winmove-axioms-draw.n3:
# :m a :DrawNode.
# :m a :DrawNode2.
the result reduces to
******
-----------------------------------------------------------------
| C | W | L | D | D2 |
=================================================================
| <foo://bla/DrawNode> | | | | |
| | <foo://bla/a> | | | |
| | <foo://bla/d> | | | |
| | <foo://bla/b> | | | |
| | <foo://bla/c> | | | |
| | <foo://bla/i> | | | |
| | | <foo://bla/k> | | |
| | | <foo://bla/j> | | |
| | | <foo://bla/f> | | |
| | | <foo://bla/e> | | |
| | | <foo://bla/l> | | |
-----------------------------------------------------------------
Successfully printed 11 query results.
Finished.
*****
It is correct that the DrawNodes cannot be derived in this case, but the
class equivalence DrawNodes==DrawNodes2 should still hold by its
characterizations.
Even more weird: when I collect all files in one (attached winmove-all.n3),
and run winmove-all.sparql, it takes much longer, and the result is only
****
----------------------------------------------------------------------------------------
| C | W | L | D | D2 |
========================================================================================
| <foo://bla/DrawNode> | | | | |
| | <foo://bla/a> | | | |
| | | | <foo://bla/m> | |
| | | | <foo://bla/h> | |
| | | | | <foo://bla/m> |
| | | | | <foo://bla/h> |
| | | <foo://bla/j> | | |
| | | <foo://bla/f> | | |
----------------------------------------------------------------------------------------
Successfully printed 8 query results.
Finished.
****
where even won and lost nodes are missing (e.g., it finds :a as win, but
not i which should be much simpler).
Best,
Wolfgang
-------------- next part --------------
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix : <foo://bla/>.
:Node a owl:Class; owl:equivalentClass
[ a owl:Class; owl:oneOf (:a :b :c :d :e :f :g :h :i :j :k :l :m)].
:edge a owl:ObjectProperty; rdfs:domain :Node; rdfs:range :Node.
:out a owl:DatatypeProperty.
:a a :Node; :out 2; :edge :b, :f.
:b a :Node; :out 3; :edge :c, :g, :k.
:c a :Node; :out 2; :edge :d, :l.
:d a :Node; :out 1; :edge :e.
:e a :Node; :out 1; :edge :a.
:f a :Node; :out 0.
:g a :Node; :out 2; :edge :i, :h.
:h a :Node; :out 1; :edge :m.
:i a :Node; :out 1; :edge :j.
:j a :Node; :out 0.
:k a :Node; :out 0.
:l a :Node; :out 1; :edge :d.
:m a :Node; :out 1; :edge :h.
-------------- next part --------------
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix owl11: <http://www.w3.org/2006/12/owl11#>.
@prefix : <foo://bla/>.
#:m a :DrawNode.
#:m a :DrawNode2.
owl11:disjointUnionOf a owl:AnnotationProperty.
:edge rdfs:domain :Node; rdfs:range :Node.
:Node a owl:Class;
owl:equivalentClass [a owl:Class;
owl11:disjointUnionOf ( :WinNode :LoseNode :DrawNode )].
:WinNode a owl:Class; owl:intersectionOf ( :Node
[a owl:Restriction; owl:onProperty :edge; owl:someValuesFrom :LoseNode]).
:LoseNode a owl:Class; owl:intersectionOf ( :Node
[a owl:Restriction; owl:onProperty :edge; owl:allValuesFrom :WinNode]).
:DrawNode a owl:Class.
:DrawNode2 a owl:Class; owl:intersectionOf ( :Node
[a owl:Restriction; owl:onProperty :edge; owl:someValuesFrom :DrawNode2]
[a owl:Restriction; owl:onProperty :edge;
owl:allValuesFrom [ a owl:Class; owl:unionOf (:DrawNode2 :WinNode)]]).
-------------- next part --------------
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix : <foo://bla/>.
:DeadEndNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 0],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 0].
:OneExitNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 1],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 1].
:TwoExitsNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 2],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 2].
:ThreeExitsNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 3],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 3].
-------------- next part --------------
prefix owl: <http://www.w3.org/2002/07/owl#>
prefix : <foo://bla/>
select ?C ?W ?L ?D ?D2
from <file:winmove-graph.n3>
from <file:winmove-axioms-draw.n3>
from <file:winmove-closure.n3>
where {{:DrawNode owl:equivalentClass ?C} UNION
{?W a :WinNode} UNION
{?D a :DrawNode} UNION
{?D2 a :DrawNode2} UNION
{?L a :LoseNode}}
-------------- next part --------------
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix owl11: <http://www.w3.org/2006/12/owl11#>.
@prefix : <foo://bla/>.
:m a :DrawNode.
:m a :DrawNode2.
owl11:disjointUnionOf a owl:AnnotationProperty.
:edge rdfs:domain :Node; rdfs:range :Node.
:Node a owl:Class;
owl:equivalentClass [a owl:Class;
owl11:disjointUnionOf ( :WinNode :LoseNode :DrawNode )].
:WinNode a owl:Class; owl:intersectionOf ( :Node
[a owl:Restriction; owl:onProperty :edge; owl:someValuesFrom :LoseNode]).
:LoseNode a owl:Class; owl:intersectionOf ( :Node
[a owl:Restriction; owl:onProperty :edge; owl:allValuesFrom :WinNode]).
:DrawNode a owl:Class.
:DrawNode2 a owl:Class; owl:intersectionOf ( :Node
[a owl:Restriction; owl:onProperty :edge; owl:someValuesFrom :DrawNode2]
[a owl:Restriction; owl:onProperty :edge;
owl:allValuesFrom [ a owl:Class; owl:unionOf (:DrawNode2 :WinNode)]]).
:DeadEndNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 0],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 0].
:OneExitNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 1],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 1].
:TwoExitsNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 2],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 2].
:ThreeExitsNode a owl:Class; rdfs:subClassOf :Node;
owl:equivalentClass [ a owl:Restriction; owl:onProperty :out; owl:hasValue 3],
[ a owl:Restriction; owl:onProperty :edge; owl:cardinality 3].
:Node a owl:Class; owl:equivalentClass
[ a owl:Class; owl:oneOf (:a :b :c :d :e :f :g :h :i :j :k :l :m)].
:edge a owl:ObjectProperty; rdfs:domain :Node; rdfs:range :Node.
:out a owl:DatatypeProperty.
:a a :Node; :out 2; :edge :b, :f.
:b a :Node; :out 3; :edge :c, :g, :k.
:c a :Node; :out 2; :edge :d, :l.
:d a :Node; :out 1; :edge :e.
:e a :Node; :out 1; :edge :a.
:f a :Node; :out 0.
:g a :Node; :out 2; :edge :i, :h.
:h a :Node; :out 1; :edge :m.
:i a :Node; :out 1; :edge :j.
:j a :Node; :out 0.
:k a :Node; :out 0.
:l a :Node; :out 1; :edge :d.
:m a :Node; :out 1; :edge :h.
-------------- next part --------------
prefix owl: <http://www.w3.org/2002/07/owl#>
prefix : <foo://bla/>
select ?C ?W ?L ?D ?D2
from <file:winmove-all.n3>
where {{:DrawNode owl:equivalentClass ?C} UNION
{?W a :WinNode} UNION
{?D a :DrawNode} UNION
{?D2 a :DrawNode2} UNION
{?L a :LoseNode}}
More information about the Pellet-users
mailing list