Test test test

My little reasoner project hit a milestone today: it terminated in reasonable time (2 minutes or so) on one of the EL variants of Galen.

Yay! No more unboundedly growing to do lists!

And it wasn’t anything clever! No change in the balance of SQL and Python!

Nope, first I refactored so I would be able to more systematically explore variants and then I finally wrote some super basic tests. Eg

A=>B. B=>C.

I did this because I should and because I suspect some subtle unsoundness was causing the unbounded growth.

It wasn’t subtle problems but blatant, serious ones. I mean trouble with retrieving chains and reasoning with conjunctions.

Fixing them fixed the leak. I don’t know if the Galen classification is correct (yet) but I have a hell of a lot more confidence. And it terminates in reasonable time!!

So simple testing pays off again.

Ideas Not Working Out (or WILL THEY?!?!?)

Well this is a bit discouraging. I was experimenting with implementing an ELK style EL classification oriented reasoner primarily using SQLite. I love SQLite and it is super cool. I want to do more with it. If you look at the algorithms in the Incredible ELK paper you see that they involve a fair number of joins and indexes, etc. They even discuss join order and reference some attempts to implement on a database. I figured using SQLite in memory databases could be a nice win.

Nope nope nope nope. Well, not yet. The problem is that it’s way to slow to interact with the database. Consider:

43393 loops done in 1.2992407480875652 minutes
    3224564 function calls in 77.975 seconds

    Ordered by: internal time

    ncalls tottime percall cumtime percall filename:lineno(function)
    183895 70.709 0.000 75.125 0.000 {method 'execute' of 'apsw.Cursor' objects}
...
    28951 0.079 0.000 34.495 0.001 calf.py:443(in_subs)

I’m testing for whether a subsumption in my todo list is in the closure. I’m using a query:

SELECT 1 FROM subs 
WHERE subclass = ? and superclass = ?

Ok that should probably be an EXISTS, but still. It’s called a fair bit (28,951 times!).

My subsumptions here are just binary tuples of integers, so I can use a Python set to track ’em easily enough. And here’s the results:

43393 loops done in 0.6202206969261169 minutes
    2819244 function calls in 37.231 seconds

    Ordered by: internal time

    ncalls tottime percall cumtime percall filename:lineno(function)
    154944 32.796 0.000 35.274 0.000 {method 'execute' of 'apsw.Cursor' objects}
...
    28951 0.025 0.000 0.053 0.000 calf.py:443(in_subs)

Well that leaves a mark.

It’s an in memory database and I’ve dorked with the transactions and no joy.

Now it’s not hopeless maybe. Consider these:

  22592   0.320 SELECT ?, superclass FROM concIncs  WHERE concIncs.subclass = ?
  22591   0.302 SELECT type, arg1, arg2 FROM IdxConcept WHERE id=?
  22592   0.180 INSERT INTO subs VALUES (?, ?)
  14442   0.141 SELECT 1 FROM inits WHERE id = ?

Same order of magnitude of queries. Sometimes returning more data. The INSERTs into subs are pretty fast. Is it just the conjunction?

Oh crap. I didn’t have a primary key on subs. It’s compound and I forgot…D’OH! Let’s fix that and…

43393 loops done in 0.14656875133514405 minutes
         3224564 function calls in 8.811 seconds

   Ordered by: internal time

   ncalls  tottime  percall  cumtime  percall filename:lineno(function)
   183895    6.106    0.000    7.675    0.000 {method 'execute' of 'apsw.Cursor' objects}
...
   28951     0.033    0.000    0.462    0.000 calf.py:443(in_subs)

Well, that’s much better! Game on! The links query is still a bit slow:

  22592  4.977 SELECT links.subclass as E, negExists.existential as F
               FROM  (links JOIN hier as h1 ON links.role = h1.subrole),
                     (hier as h2 JOIN negExists ON h2.superrole = negExists.role)
               WHERE links.filler = ? AND negExists.filler = ?

No obvious issues. I’m unclear whether an index will help…but stilL! Back in the game!

Renata Wassermann on Belief Revision in DLs

I used some of Renata’s work in my thesis and we’ve corresponded on and off. One of her students is visiting us and she came and gave a talk! It was very nice.

One interesting bit was that did some experiments on partial meet vs kernel based revision and found “contrary to computer science intuition” partial meet generally is more efficient. Ok that’s a lot of jargon here’s an attempt to sort it succinctly.

Given a set of beliefs, B, (think propositional sentence ie things which can be true or false), and some sentence S which follows from B, how can we shrink B so S no longer follows? This isn’t easy! S may not be a member of B. S might be entailed by lots of different parts of B.

One approach is to find all the minimal subsets of B which entail S. Since they are minimal, we can break the entailment by deleting just one element. If we fix each subset then we have a fix for B. These subsets are called kernels (or justifications). They correspond nicely to typical debugging approaches.

Alternatively, we could try to build a maximal subset of B which doesn’t entail S. There will be many such subsets but obviously each does the job. Call such a set a remainder. We can just pick one remainder, or take the intersection of several (or all). If we take fewer than all we have partial meet contraction.

Now Renata said something that didn’t make sense to me ie that the reason kernal contraction has been preferred is that computer scientists think it’s more efficient because “kernels are smaller”. But…I’ve never heard that. The concepts are dual but kernels are easier for humans to deal will. They capture the logic of how the undesired entailment works. It never occurred to me to even ask which approach is more efficient. It depends on the nature of the sets!

One interesting bit is that a difference between debugging and revision folks is that debugging folks usually consider minimal repairs, ie, selections from the set of justifications that contain no repairs. This corresponds to full meet contraction which has a number of issues. If you go for partial meet then you have to do a bit of work to get an algorithm that finds desirable contractions compared to the remainder based approach.

Of course, even from a debugging perspective a partial meet approach might make sense. When you figure out a bug, you might make more changes than just the minimum one to fix the focus broken test. After all, you might get an insight about a particular function call and change how you call it everywhere. You might realise that a module is just irredeemably broken and replace it entirely.

A Tale of 3-5 Syntaxes

Oh OWL, how you vex me.

I’m starting an implementation of a reasoner in Python (BECAUSE!!!). Which led me to the need for some internal representation of the ontologies I want to reason over. Fine. OWLReady won’t do, by design. Sigh.

So, I first think to whip out a quickly representation with tuples, maybe Named Tuples, maybe TYPED NAMED TUPLES!!! (but that’s misery for another blog post) and I start…

…but, I think, why not do a proper Python API straight off the structural spec? That’s what it was meant for. The OWL API basically follows it. It gives me “free” documentation and proves the concept. I put a lot of work into that spec, though Boris designed the functional syntax and thus the API (and Boris and I have been fighting over APIs since the first time we met!)

I’ve sketched out a partial set of syntactic forms following the OWL API in Python which gives me, essentially, new, evaluable, literal forms. Let’s compare to other syntaxes!

For comparison, I’ll use a four axiom, EL ontology taken from the ELK paper (example 1 on page 6). It’s small. It’s not complex. So yay!

German/Math syntax

This is what you see in most papers. No one parses it.

    A ⊑ ∃R.(C ⊓ D)
    B ≡ A ⊓ ∃S.D
    ∃S.D ⊑ C
    R ⊑ S

Awesome. Clear. Easy to read. Somewhat annoying to type.

Jewel

Jewel is a syntax I came up with designed to be close to German syntax (with a Model Logic twist) and very typeable. I have a parser but haven’t used it in aeons.

A => <R>(C & D).
B = A & <S>D.
<S>D => C.
R ==> S.

IT’S PRETTY DAMN FINE!

Easyish to parse. Almost as short as German. Easy to read. Excellent.

Adhoc Wordy DLish StrucSpec Like

Using named tuples, I threw together a little wordy syntax that mapped directly into the corresponding Python structures:

[
  Subconcept(Concept('A'), Exists(Role('R'), And(Concept('C'), Concept('D')))),
  Subconcept(Concept('B'), And(Concept('A'), Exists(Role('S'), Concept('D')))),
  Subconcept(And(Concept('A'), Exists(Role('S'), Concept('D'))), Concept('B')),
  Subconcept(Exists(Role('S'), Concept('D')), Concept('C')),
  Subrole(Role('R'), Role('S'))
]

Could be worse! I latched on to the DL terms “concept” and “role” because that was what I was reading, but what I’d gain with “class” I lose with “property” so it’s fine. Maybe I could use one letter names for the atomics:

[
  Subconcept(C('A'), Exists(R('R'), And(C('C'), C('D')))),
  Subconcept(C('B'), And(C('A'), Exists(R('S'), C('D')))),
  Subconcept(And(C('A'), Exists(R('S'), C('D'))), C('B')),
  Subconcept(Exists(R('S'), C('D')), C('C')),
  Subrole(R('R'), R('S'))
]

And really, it could be “Sub” if I’m going to type all the vocabulary.

Not terrible. Okish to type. Automatic parsing. Deviates from everything.

OWL Structural Spec

I’m just going to do the first axiom because I lost the will to live:

owl.SubClassOf(axiomAnnotations=None,
               subClassExpression=owl.Class(entityIRI='A'),
               superClassExpression=
                   owl.ObjectSomeValuesFrom(
                       objectPropertyExpression=owl.ObjectProperty(entityIRI='R'),
                       classExpression=owl.ObjectIntersectionOf(
                               owl.Class(entityIRI='C'), 
                               owl.Class(entityIRI='D'))

OY! I could get rid of the owl with a tweak to imports (i.e., to the bad practice of from owl import *), but that’s only going to help a little. How I hate all those redundant “objectProperty”s.

I hated literally every moment of typing out this one axiom, even with autocomplete. Reading it makes me want to throw up. I can’t imagine that programming with it would be nice.

Let’s see what happens if I add the prefix to the ad hoc one:

owl.Subconcept(owl.C('A'), owl.Exists(owl.R('R'), owl.And(owl.C('C'), owl.C('D')))),

Ooo, that sucks. Maybe killing the prefix will save the day?

SubClassOf(axiomAnnotations=None,
               subClassExpression=Class(entityIRI='A'),
               superClassExpression=
                   ObjectSomeValuesFrom(
                       objectPropertyExpression=ObjectProperty(entityIRI='R'),
                       classExpression=ObjectIntersectionOf(
                               Class(entityIRI='C'), 
                               Class(entityIRI='D'))

So, I don’t think I’m going to continue with the strict conformance to the naming scheme of the Structural Spec.

Posted in OWL

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.

Posted in OWL

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.