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).