Thinking Clearly .

Hans Rosling is someone I want to take a course from (hey! he has a weblog). He is an amazing speaker, as can be seen in his 2006 talk Myths about the developing world (given about a year ago). (Hat tip to lemonoder for the link.) He’s funny, witty, deep, and engaging…what a treat to watch! The viz tool he used is available and he uses it very well. I poked at it and it’s pretty darn easy to use. (I was fascinated by carbon dioxide emissions per capita vs. income per capita. I tracked China, Iran, Hungary, Japan, the UK, and the US. You might want to try a linear scale on the y-axis.)

At the end of his talk, he spoke of the need to make the data searchable. He has the front ends, but data access is a big issue. Semwebbers, let us step up! Forget our favorite tool or language! This is what we should want to see and help make happen however we can!

Yay! Hurray! My first snow as a resident of the UK!

(Though not my first snow in the UK.)

Today we had hail, rain, bright sun, and crazy snow….very nifty. And last week we had the “oh wow” winds. As in, “Oh wow, I have to downshift in order to turn the pedals on my bicycle.” Now, it is, of course, a testimony to my wimpdom that I could be stopped dead by a little, ok, a lot, of very fast wind. But still!

On the SPARQL front, I am participating in Yet Another SPARQL Tutorial, but this time it’s a full day and seems rather sensible. Hosted by ESWC 2007, and co-presented with a slew of good folks (Axel Polleres organized it, though some of the other folks were putting together submissions as well). I think it’ll be nice with lots of interesting information.

Coincidentally, Axel has put together a worked out SPARQL Rules proposal. This isn’t too shocking, especially given the presence of CONSTRUCT, but it’s very nice to have it worked out. Folk wisdom is ok, but details drive the devil away. It’s an interesting thing to experiment with.

My bit will be, as one might expect, SPARQL over more expressive entailment regimes (through OWL), plus, I hope, a bit about different ways of interpreting results.

On a slightly related note, Michael Kay discovers some value in XQueryX (the XML syntax for XQuery), albeit with the amusing twist that he finds manipulating XQueryX to be the proper domain of XSLT.

Kendall and I went a good chunk of the way to a SPARQLX (i.e., SPARQL XML format). Perhaps it’s time to revive it. The advantages seem to be the same: XSLT transformations to various legacy formats, the ability to indicate in advance (by a schema) what query feature you do or don’t accept (and thus better WSDL typing), better embedding in other XML formats, etc.

Our plan to offer commercial support for Pellet, and to gradually transition it from an academic to an industrial-strength tool, is proceeding nicely. OWL-DL is an interesting technology; but I keep hearing and seeing signs that the killer app still for Description Logics in Web technologies is still around the corner.

One of the things I spend my time these days doing is, well, looking for that killer app. I think at some point it will be found in the area of policy management; there is some very promising research being done in this space at UMD (and many other places), and we’re excited about our chances to roll out products in this area in the next 12 to 18 months.

But I’m also on the lookout for areas that will work now, and I’m starting to think that “collective intelligence” could turn into one of those near-term wins. What I mean in particular is creating an argument or decision-support tool, using OWL-DL and Pellet, within a public policy web app, like a prediction market, policy-support tool, social-network analysis, etc.

I recently happened upon an interesting paper in this area, “Collective Intelligence for Decision Support in Very Large Stakeholder Networks: The Future US Energy System”, which describes a web app to be used in stakeholder networks, with the example domain being the energy market in the US. Now, the web app part isn’t novel: it’s roughly equal parts wiki and polling system. The novel bits are what we might call the social informatics, that is, the structure of the interaction process and that these kinds of systems are being seriously considered and, in some institutions, deployed.

Of particular note for Clark & Parsia as an R&D company is the fact that the web app is designed to allow the use of an automated tool for supporting human decision-making processes, including argumentation analysis. Now this makes me happy for at least four reasons:

1. we’re interested in what I call (I hope not idiosyncratically) “hard collective intelligence”, that is, computer-aided collective intelligence using description logics, machine learning, or other AI and KR approaches. Someone’s gotta do the soft CI work, but we’re not ready to start hiring sociologists just yet…;


2. in the US, anything that contributes to increased rationality in public policy deliberation can only be a good thing;


3. it’s precisely the kind of work we want to be doing; and


4. it’s the sort of work that will dovetail nicely with our policy management schemes, which include things like dedicated policy management appliances embedded in the enterprise fabric, and SDKs for policy-to-logic mappings, etc.

We are and will remain for some time, perhaps a long time, a description logic company; but we’re also very excited by all the great work happening in machine learning, social and network informatics, computational economics, etc. It’s a great time to be working in all of these areas, and I’m especially interested in all the overlaps and interstices. If you’re doing this kind of work towards a degree, you might want to drop us a line; we’re always looking for graduate students whose research we want to support, since they make great partners and even better employees.

At OWLED 2006, the attendees decided that we should try for a working group to standardize
the OWL 1.1 documents as a set of W3C recommendations. The next step in producing a working group is
to produce a working group charter. Since, I started a very sketchy charter draft for discussion at OWLED, it seemed to make sense to flesh it out as a starting point. I’ve started a discussion thread on public-owl-dev about it.

I tried to write a (draft of a proposal for a) charter that is sufficiently scoped so
that the working group is constrained to a relatively small,
predictable addition to OWL. I personally want this for several reasons:

• As an implementor, expert, and tool guy, I hear a lot of “we need qualified number restrictions”, “Should I use OWL Lite?”, and “Why can’t I use the Dublin Core ontology with OWL DL?” Of course, I also hear, “How about rule support?”, “Database integration!”, and “How about nonmonotonic inheritance?” (Ok, the last not so often :)). The difference for me between the former and the latter is the former are more semantically and implementationally uncontroversial (though, punning and annotations are possibly dodgy semantically), and I know enough high profile, high value users who would, in fact, use the particular variants that we can easily build consensus and implementations around. So, I would like to implement support for them in an interoperable and standardized way.
• While people have mentioned worries about disturbing the OWL and Semantic Web ecology by somehow sending the message that “OWL is broken” or “Wait for the new and better OWL before adopting”, I think there is a converse worry: that OWL should appear to be stagnant, and/or that persisting missing functionality (esp. QCRs and Datatypes) will drive important users away from OWL. Clearly, neither consideration is conclusive since they are both predicated on rather tenuously based predictions. However, I hope that this working group will balance the concerns. By being scoped and incremental and fast, I hope it can avoid any untoward destabilization. Old OWL will still be good OWL. Having major tool builders on board also helps a lot. (I think we’ll get some new vendors too, esp. given the tractable fragments document.)
• I dearly hope this is not the last increment/addendum/change to OWL. I hope this group can set the bar for useful, careful additions to be quite low. At the moment, afaict, there’s no (other) plan or intention for adding to OWL. Given the wealth of interesting and useful extensions being developed, the postponed issues, and the partially met or unmet goals of WebOnt (not to mention the goals they left out!), it seems clear that just punting is a non-starter. I’d like there to be a clear way forward. Personally, I’d like to repeat what we did for this: At an OWLED, discuss what’s the next sensible de facto standard. Once that is realized, form a working group to make the de facto all de jure.
• Some things can be and perhaps properly are handled by other groups, such as the RIF (for rules; though really, the RIF is about interchange of rules and what some OWL users want is an OWL rules language, which might then have a corresponding RIF dialect), or the DAWG (for conjunctive query). But other things really seem to require attention on OWL itself (such as QCRs, axiom annotations, and the like).
• I would like OWL to be a bit more XML friendly, on the one hand, and human reader friendly, on the other. I think these can help adoption a lot by reaching into new user communities.
• Logic based KR has a lot to offer that OWL or OWL DL (and, by extension, OWL 1.1) doesn’t offer. There are competitors, both standardized or standardizing (e.g., Common Logic) or not (F-Logic), that are worthy of respect and investigation. There are choices running fairly deep in OWL (and OWL DL) that make synthesis with these other languages, at least as they are commonly implemented and deployed, fairly nontrivial. In fact, there is ongoing research on this. I don’t want this working group to address any such issues, mostly because I don’t, at the moment, as a tool developer, see how to support what I imagine the resulting specs to be in any reasonable time frame for a reasonable (and likely) level of investment. Heck, I don’t see how to specify such in a reasonable time frame for a reasonable level of investment.
• I would like the working group to finish in short order. So, I’m trying to make the charter such that the working group doesn’t go off into the weeds (my experiences with WSDL and DAWG loom; even WebOnt and RDF Core are cautionary). On the other hand, I’ve been on the short end of a charter fight where, really, we could just fix something or add something really useful, but “the charter doesn’t allow it”, while not typically actually a show stopper, makes it all very unpleasant and tedious. I would like the charter to be helpful to the group, not annoying to it, and helpful to reaching completion in a short time frame.

These were the sort of thing running through my head as I tried
to craft a charter.

There’s a streamline version of these considerations prepended to the draft. I felt compelled to write out these thoughts to help avoid confusion about the “status” of this draft. It has no official status with anyone. I wrote most of it. Ian reworked large chunks. I think it reasonably reflects the understanding of the attendees at OWLED 2006. And, I think it’s a reasonable charter. I could live with this. If you have radically different goals, then you may not be able to live with it. Tant pis. Come to OWLED and influence the next one!

I see Dan has converted the Witch argument to N3 and used its proof generation tools to output a proof (btw, Dan, the OWL version was a solo effort by me and I guess you’ll have to come to our actual weblog to see who I am :)). (BTW, even though I linked to it, I should mention explicitly that the original is due to John Ioannidis.)

I’m jotting up the tableau version of the proof (but it’s a bit tricky, pedagogically since if I use a linear proof format, then it doesn’t really correspond to what, e.g., Pellet does, but if I use a completion graph approach I gotta go graphical). However, Dan’s post reminded me that SPASS (and MSPASS) will generate (roughly, resolution based) proofs and have web interfaces. (These proofs are meant, I think, to be checkable.)

So, following the SPASS tutorial, I got this:

begin_problem(Burn_the_Witch_Argument).

list_of_descriptions. name({*Burn the Witch Argument <strong>}). author({</strong> Bijan Parsia <strong>}). status(unsatisfiable). description({</strong> Formalization of the Burn the Witch Argument*}).
end_of_list.

list_of_symbols. functions[(girl,0), (duck,0)]. predicates[(Burns,1),(Woman,1),(Witch,1),(IsMadeOfWood,1),(Floats,1),(SameWeight,2)].
end_of_list.

list_of_formulae(axioms). formula(forall([X], implies(and(Burns(X), Woman(X)), Witch(X))), 1). formula(Woman(girl),2). formula(forall([X],implies(IsMadeOfWood(X), Burns(X))),3). formula(forall([X],implies(Floats(X), IsMadeOfWood(X))),4). formula(Floats(duck),5). formula(forall([X,Y],implies(and(Floats(X), SameWeight(X, Y)), Floats(Y))),6). formula(SameWeight(duck, girl), 7).
end_of_list.

list_of_formulae(conjectures). formula(Witch(girl),8).
end_of_list.
end_problem.

If you paste this into the SPASS interactive web form, and add -DocProof in the options field, you’ll get a bunch of stuff including the proof:

Here is a proof with depth 3, length 15 : 1[0:Inp] || -> Floats(duck)*. 2[0:Inp] || -> Woman(girl)*. 3[0:Inp] || -> SameWeight(duck,girl)*. 4[0:Inp] || Witch(girl)*+ -> . 5[0:Inp] Floats(U) || -> IsMadeOfWood(U)*. 6[0:Inp] IsMadeOfWood(U) || -> Burns(U)*. 7[0:Inp] Burns(U) Woman(U) || -> Witch(U)*. 8[0:Inp] Floats(U) || SameWeight(U,V)*+ -> Floats(V). 9[0:Res:7.2,4.0] Woman(girl) Burns(girl) || -> . 10[0:MRR:9.0,2.0] Burns(girl) || -> . 17[0:SoR:10.0,6.1] IsMadeOfWood(girl) || -> . 18[0:SoR:17.0,5.1] Floats(girl) || -> . 20[0:Res:3.0,8.1] Floats(duck) || -> Floats(girl)*. 21[0:SSi:20.0,1.0] || -> Floats(girl)*. 22[0:MRR:21.0,18.0] || -> . Formulae used in the proof : 5 2 7 8 4 3 1 6

Neat!

SPASS is a full first order logic theorem prover. Our translation into OWL DL (ALC really) shows that we don’t need full FOL for this. MSPASS tweaks SPASS so that it effects a decision procedure for (various) DLs. I did a MSPASS DL variant of the argument as well (wish I had an tool to convert to that format from OWL; oh, if you want to save it to disk, you should strip off the ”.txt” and put a dot before the “dfg”.). You can test it with the MSPASS web interface (which will show you the various translations back to FOL).

Philosophically, I’m remain skeptical about the general value of proof generation (at least for exchange, e.g., for PCA like tasks), especially for scalable, decidable logics. Basically, the proofs can be expontential in the size of the input, and the input can be large. For decidable logics with optimized reasoners, for many things, an asserted justification (i.e., a minimal set of axioms from the KB sufficient to entail the conclusion) might be more than sufficient. There’s a complex story here, of course, but if your proof checker isn’t reliable (Dan said he was still finding bugs :)), then even using it to verify is a bit tricky. Proof checkers aren’t always easier.