OWLReady Not Ready For Me

Every now and again I see a new OWL oriented library for a language I use and I get excited. I’d love to have something equivalent to the OWL API in Python! And look! There’s OWLReady! OWLReady2 even! It parses multiple syntaxes, uses sqlite as a store, connects to HermiT for reasoning, has some SPARQL support…YAY! It even has some interesting looking Python-OWL integration. YAY!

Or rather boo. It’s not axiom oriented. It doesn’t follow the structural specification. Further more, the module structure is confusing and I think I’ve already hit some major bugs. Given how far away it is from the axioms, it seems unlikely as a focus for collaboration.

This makes me sad! I wish them well. The developer certainly was nice enough.

Advertisements

Ontology Management on the Gartner Hype Cycle!

The Gartner hype cycle is an analytical construct (of sorts) which tries to capture the relation between a technology and the expectations we have for that technology. It’s based on the pretty reasonable observation that esp with new technology, there’s a tendency for expectations to outrun the current or even potential benefits. Everyone wants to use the new glittery magic, so vendors and specialising consultants do very well for a while. But it turns out that the new technology isn’t magic, so people find that they’ve spent a bunch of money and time and energy and they still have the problems the tech was supposed to magically solve. This leads to a crash in expectations and a backlash against the tech. But lots of new tech is actually useful, used appropriately, so some of the new tech, its shiny worn off, finds a place in our toolkit and tech landscape. The Gartner hype cycle is a pretty iconic graph with fun-ish labels:

(The y-axis gets different labels over time.)

And people try to operationalise it:

Hype-Cycle-General.png

But I’m skeptical about a lot of this as being rigorously evaluate.

Of course, sometimes a tech takes off and doesn’t really stop. It goes pretty straight from trigger to productivity. The iPhone/iPhone style phones comes to mind. It Just Grew. It may level off as it hits saturation, but that’s a completely different phenomenon.

This is all pretty banal stuff, but Gartner takes it very seriously (they’ve branded it!).

ANYWAY, this year’s hype cycle, excitingly, includes ontology management for the first time! WE’RE ON THE MAP!

  • 16 new technologies included in the Hype Cycle for the first time this year. These technologies include 4D Printing, Blockchain, General-Purpose Machine Intelligence, 802.11ax, Context Brokering, Neuromorphic Hardware, Data Broker PaaS (dbrPaaS), Personal Analytics, Smart Workspace, Smart Data Discovery, Commercial UAVs (Drones), Connected Home, Machine Learning, Nanotube Electronics, Software-Defined Anything (SDx), and Enterprise Taxonomy and Ontology Management,

Alas, if you look at the graph, we’re on the downslope into the Trough of Disllusionment:

And it has a “more than 10 years” to mainstream adoption label.

Ouch!

This is discouraging and perhaps hopeful. Remember that the hype cycle doesn’t tell you much about the qualitymaturity, or utility of the technology, only the perception and influence of perception on the market. (To the degree you believe it at all.) 10 years to mainstream adoption is not 10 years from being a boon for your business or a viable business itself. It means you will often have a hard sell, because people are skeptical.

Update: Oh WordPress. Picture management please.

Recent Keynotes

It’s not often that I can have a post about my doing any sort of keynote…depending on how you count, I’ve only done one or maybe two before 2015. Then there were two in 2015!

The first was at OWLED. This year I went heavily (again) for HTML based slide decks, so you can browse my reveal.js slides (with an embedded timeline!). This was, obviously, about the Web Ontology Language past and possible future.

The second was at SWAT4LS and it was a call to take on the challenge of representing all medical knowledge.

Both were very well received. I hope to do a video of the SWAT4LS one as I had several requests to replicate the full experience.

There’s a fair bit of overlap between the two because I am currently fairly obsessed with the problem of representing and sharing evidence.

Both of these, OF COURSE, involved all nighters. The writer’s block thing is tough.

But, I give a pretty good talk! I would do more keynotes (hint hint).

So many keynotes are just horrific. I got to the point where at many conferences, like ISWC, I just don’t go because they are so insultingly terrible I lose it. (Ron Brachman gave an epically awesome on at DL. Marvin Minksy gave an epically awful one at AAAI.)

Keynotes can be great because they give space to do something different. You don’t have to report on a paper. You can explore an wacky idea. Or synthesise some history. This is actually a cool part of dissertations: You have the room and the right to put things down that don’t fit anywhere else. Keynotes should be like that. I don’t want a fluff piece or giant pile of ego boo. I want something interstitial…vicera which pull the research organs into place. It doesn’t have to be profound. It doesn’t have to be controversial. (Though that can be good.) But it should be distinctive and preferably fun!

(See this earlier post about my speaking anxiety.)

More New OWL Syntax

Thus far, I like my New OWL Syntax (though it needs a name). I think the key refinement though is in the counting quantifiers. The slashes just didn’t work, so we have curly brackets with the numbers paired with the right or left one depending on whether you want max, min, or both.

So, a rough grammar

Sub ::= =>
Equiv ::= =
AxiomConnective::= Sub | Equiv
Quantifier ::= Existential | Universal | Counting
Existential ::= <Role>
Universal ::= [Role]
Counting ::= {number Role} 
      | {Role number} 
      |  {number Role number}
Restriction ::= Quantifier Concept
ConjOrDisj ::= Concept (& | v) Concept (parens if needed)
Negation ::=  ~Concept
Concept ::= Restriction | ConjOrDisj | Negation | name
TBoxAxiom ::= Concept AxiomConnective Concept.
ABoxAxiom ::= name:Concept | <name, name>:Role
Role ::= name.

So this gets us ALCQ. An example (some axioms ripped from Koala, I don’t have nominals yet):

Parent = Animal & {1 hasChildren}Thing.
DryEucalyptForest =>Forest.
Koala => Marsupials & <hasHabitat>DryEucalyptForest.
Marsupials => ~Person.
Animal => {1 hasHabitat}Thing & {1 hasGender 1}Thing.
StudentWith3Daughters = Student 
               & ([hasChildren]Female 
                                  & {3 hasChildren 3}Thing)
fluffy:Koala.
<fluffy, sandy>:hasChildren.

I’m not thrilled by my stealing of the nominal constructor ({}). I thought about reusing <> and [] (just adding numbers). This works really well for the existential (since a min N really is N somes, plus a little), but max isn’t that close to the universal for most people. Another problem is that using & and angle brackest means using the corresponding entities in HTML or XML which is a common typing place for me.

Binary and and or can be annoying as well.

Posted in OWL

New OWL Syntax

I’ve been obsessing a bit about artificially generated satisfiability problems (KSAT). The work in propositional logic really is outstanding and, upon revisiting, the work in modal and description logics is pretty interesting (after some mis-steps). Pavel and I have been doing similar experiments for probabilistic SAT (both propositional and SHIQ based). People are often annoyingly dismissive of such experiments. (Grumble about one review that killed our last paper.) But that’s not what I’m after today.

As I wish to do experiments, I need generators (there’s analytic work as well, of course). So I’m writing some. Or starting to. Since I want to use OWL reasoners, it makes sense to target OWL. This is a bit tricky as OWL doesn’t directly accommodate concepts by themselves (you need axioms). Now, of course, we can use the expression syntax of OWL/XML or even of OWL/RDF (shudder), but these won’t be legal OWL files. One can, of course, hack around this using class assertions or the right subsumption axioms (and I plan to do all that). But it’s awfully verbose and not very descriptive (e.g., no tag says “clause”). So, I thought about designing a new XML format which I could then write translators over.

It’s verbose. Nastily nastily verbose. If you look at the DIMACS SAT problem format, you get a sense of what a mess this all is. Of course, DIMACS just uses numbers for variable names, But Still.

I could use Manchester Syntax, but it’s a bit awkward on a number of fronts. I want something typeable and which looks reasonably like so-called “German” DL syntax. So, here’s a sketch, first restricting to ALC. An example:

Person = Parent v ~Parent.
Parent = <hasChild>Person.
[hasChild]Happy & Parent => HappyParent.
Parent != Childless.
Childless = ~Parent.

So this is a simple TBox. The sentential operators are the usual v, &, and ~ (for or, and, and not, resp.). The quantifiers are modeled after the modal possibility (diamond, existential) and necessity (box, universal) operators with their “grading” (property) inside. The conditionals, I’m less sure of. I think I prefer “=” for equivalence to “” or “”. It reads naturally. But then implication feels a touch hacky. Perhaps “->” would be better. “!=” is sugar for disjointness and I want that for the n-ary case.

Quantifiers bind tightly so if you want HappyGrandparent, you need parentheses:

[hasChild](Happy & Parent) => HappyGrandParent.

For the ABox, I’m torn between classic so-called German style and first order functional style:

maria:Parent.
<maria,bijan>:hasChild.

Parent(maria).
hasChild(maria,bijan).

German style has a minor readability advantage for class assertions (maria isa Parent). I guess we could mix them.

Things get interesting with the counting quantifiers. I want to keep the quantifier style consistent, which has led to the following design using the delimiters /../ for at least, \..\ for at most, and |…| for exactly:

/2 hasChild/Hyper => FrazzledParent.
|1 hasChild|Person = ParentOfOnlyChild.
BelowReplacementFamily = \2 hasChild\Person

Yeah. The exactly seems fine. The intuition I’d give for min and max is that if the slant is rising that indicates a fan out of successors, whereas if it is descending, it indicates a cap.

I suppose I could use the pipe + “min” and “max” (or even > and < but then we need equals and it gets messy or confusing).

Posted in OWL

Explanation of “Progress?”

So, my post Progress? was snark and a bit insidery at that. Given that I’ve already had one person give me the puzzled comment about it, it seems right to give in and just dissect the damn frog already.

In ontology circles, esp. of the description logic variety, “explanation” is a key feature of knowledge based systems. Sometimes you hear the story of how the early expert system, Mycin, would diagnose with high reliability but doctors wouldn’t accept those diagnoses. Then they added an explanation facility and suddenly doctors would accept it. Thus, explanation is necessary to trust the system. (There’s actually some reasonable empirical evidence to show this for even modern expert systems, e.g., for financial analysis.)

Since early forms of explanation were essential “traces” of the system reasoning, it’s an easy step to say that explanations are “proofs”. This also hooks up with Hempel’s deductive nomological model of scientific explanation (i.e., a deductive argument with at least one scientific law as a premise).

However, when we talk ontology engineering, and esp. various debugging tasks, the most successful form of explanation has been so-called (and so-called by me, alas) justifications, that is, minimal subsets of the original theory which suffice for an entailment to hold.

Stefan Schlobach (and friends) almost certainly gets priority in the 2000, with loads of antecedents in and out of the DL community. Aditya, Evren, and I sorta reinvented them when trying to produce something from Pellet for the InferenceWeb system, and never looked back.

Borgida (the fellow I’m pretty sure I was quoting) had some work on explanation that was more proof oriented. This rather recent paper picks that up. At a DL workshop (where the first, more categorical paper was given) he got some push back (I’m pretty sure from me). The later paper is less categorical.

In the end, I really hope that people get away from the “Proofs are explanations, the best explanations, and the only explanations” mindset. I don’t think it’s fruitful.

On Facebook, Enrico again tried to frame everything in terms of proofs in some (perhaps varying) system or partial proof in a given system (the latter is super weak given we have decision procedures…every entailment has a finitely findable proof, so any string of lemmas is trivially convertible into a partial proof, in some sense).

But this is really analytically bogus. It’s unclear what benefit comes from reducing everything to proofs, partial or otherwise. (And what about model based explanations, esp. for non-entailments? Or analogical explanations such as with case based reasoning? And justifications really really are “just the premises”.) Does this clarify anything? Don’t we just reinvent the distinctions we want inside the framework (e.g., with partial proofs)? I certainly do not see how it would help Borgida et al, after all, there is no dialectical point in stressing that explanations are proofs when bolstering a fairly specific kind of proof as explanation if the first occurrence of proof provides almost no constraints.

In the end, I’ve no doubt that proofs can serve, even in the ontology engineering setting, some explanatory purposes. Heck, I’m researching them for these purposes! I also don’t much care if other people want to be blinkered, or want to bash justifications, or what have you, at least, I don’t see such bashing (directly or slyly) as substantive criticism. I do think it’s worth sitting down and trying to understand what such statements (or beliefs) actually buy us.

My current thought is “Not much, and probably are somewhat harmful.” I’m willing to be convinced otherwise if someone has the goods.

Progress?

From, Explanation in DL-Lite presented May, 2008:

As far as explanations are concerned, it is almost universally accepted that they are formal proofs, constructed from premises using rules of inference.

From, Explanation in the DL-Lite Family of Description Logics presented November, 2008:

It is widely accepted that an explanation corresponds to a formal proof. A formal proof is constructed from premises using rules of inference.

From Progress? published November, 2009:

Proofs? Schmoofs!