Logic
Work is keeping me busy in Chicago at the moment. That's not to say that I'll write more when I get home, but I hope I will.

Yesterday I was in a meeting being told about the semantic products provided by Exeura. Exeura is a commercialization spin off from the University of Calabria, so many of the products are using new technologies that are not fielded commercially elsewhere yet. In the course of the meeting, one of the products was described to be based on "Disjunctive Logic". When queried on this, the explanation was that Disjunctive Logic is a type of logic used commonly around the world.

Now I know there are a lot of logic families, but I hadn't heard of this one. So I went looking. Funnily enough, most of the useful references I found were publications from the very people at Exeura. That's not to say they invented Disjunctive Logic, but they are some of the co-authors of the DLV project, which is one of the only disjunctive logic processing systems. I'll confess that this made me a little cautious about it's readiness for commercialization, but I'll have to reserve judgment until I see it.

I looked up Disjunctive Logic to try to learn what makes this branch of logic special. The first paper I decided to read was co-authored by the same people at Exeura, so at least I knew I'd be looking at the same thing. Almost straight away I saw the following:
Disjunctive logic programs are logic programs where disjunction is allowed in the heads of the rules and negation may occur in the bodies of the rules.

That's when the little light came on for me!

Everything I read over the next few pages was exactly what I expected to read. This is because I've been running into this all the time recently. I've been using cascading equations in ordinary description logic in order to avoid disjunctions in the heads, and here is a tool that is specifically designed to allow for that. I still have to read all the details, but I can see how useful this could be.

Sudoku
The first example of disjunctive logic that I can think of is in a non-trivial game of Sudoku. I first played this 2 weeks ago, discovering quickly that it was just a simple logic puzzle. I expect that most programmers were like me, and immediately started thinking about how to solve the puzzle with a computer program. It seems to come down to 3 simple rules, and I've noticed that the "harder" the puzzle (according to the rating system in the book I have), the more of the rules you have to employ in order to solve it.

I use the name "group" for all the squares in a 3x3 grid, a row, or a column. I'll do that here for clarity.

It's my third rule which is relevant to disjunctive logic. It states:
If there are n squares in a group which contain exactly the same n possible numbers, then those numbers are not possibilities in any other square of that group.

(Actually, there's a corollary: If there are n squares in a group which contain at least the same n possible numbers, and those n numbers appear in no other squares of the group, then any other possible numbers in those n squares may be eliminated)

So what is this saying? For instance, consider a column with several empty squares. For two of these squares we've determined that they could only be the numbers 2 or 3. That means that we know that if the contents of one square is a 2, then the other must be a 3, and vice versa. However, which don't yet know which way around. However, this is enough to tell us that no other square can be a 2 or a 3. If there were another square which had been narrowed down to being a 2 or a 5, then the 2 can be eliminated, letting us put a 5 in there.

So even though we only had partial information of the contents of 2 squares (we knew the numbers, but not which way around to put them), it was still enough to tell us how to fill in another square. This is a case of disjunctive logic, as our result (the head of an equation) was an OR between two possibilities, but this was still enough to solve for the body of the equation.

OWL
This also works with OWL, particularly the cardinality questions I was struggling with some time ago.

If a class has a restriction:

  <owl:Class rdf:ID="MyClass">
    <owl:intersectionOf rdf:parseType="Collection">
      <owl:Class rdf:ID="MyOtherClass">
      <owl:Restriction>
        <owl:onProperty rdf:resource="#myProperty"/>
        <owl:maxCardinality>2</owl:maxCardinality>
      </owl:Restriction>
    </owl:intersectionOf>
  </owl:Class>

Then objects of type MyClass can only refer to two objects with the myProperty predicate. So if I have the following:

  <namespace:MyClass rdf:about="#myClassInstance">
    <myProperty rdf:resource="namespace:A"/>
    <myProperty rdf:resource="namespace:B"/>
    <myProperty rdf:resource="namespace:C"/>
  </namespace:MyClass>

Then I know that two of A, B or C must be the same thing. eg. If A and B are the same:

  <rdf:Description rdf:about="namespace:A">
    <owl:sameAs rdf:resource="namespace:B"/>
  </rdf:Description>

Of course, the possibilities are: A=B or A=C or B=C. (where I'm using = like owl:sameAs).

So this is a similar situation to the Sudoku example. We know there are only 2 objects, but we have 3 labels for them. That means that we have partial information, but like the Sudoku example, the partial information is still useful.

The question is, how do I process this partial information? Until today I had no idea. Now it appears that Disjunctive Logic was specifically designed for this situation. :-)

Of course, this is only relevant if there is useful processing to be done. Unlike Sudoku, OWL can say lots of things with no consequences. For instance, using a predicate more often than specified in an owl:maxCardinality restriction will not create an invalid document unless there are sufficient owl:differentFrom statements to differentiate the objects. It is impossible to violate owl:minCardinality unless the range of the property is too restricted in number (an uninstantiable class, or a class of owl:oneOf). I've talked about this in the past.

So with such an open system, with the extra processing allowed by Disjunctive Logic actually gain me anything? I'm not sure yet. Give me some time to find out.