[PaulHoule]

Practically I work with SPIN. I wish somebody would make a production rules engine that was easy to live with. I want to like Drools but I can't read the error messages for complex programs I write. With Jena Rules the system is simple enough that I can figure problems out looking at the source code but it doesn't have as many features.

Unfortunately logic is a depressing subject because it starts with a bunch of theorems about what is impossible (Gödel, Tarski,Turing.) There is no system of negation that is without problems (OWL takes the radical choice of no negation) Commonsense reasoning involves a lot of "Alice thinks that Jane thinks that..." and "A was true until 12:30 this afternoon, now A is false".

The theory vs interpretation split is another one of those decisions you have to make if you want to do logic: I am on a committee where I'm the guy who speaks for interpretations and the A-Box but some of the other people are serious T-Boxers.

It amazes me that this system

http://inform7.com/

creates an illusion of letting an English major write a script for an adventure game that reads like English that someone can play in what looks like a subset of English. It does it all with a very primitive production rules engine that relies heavily on defaults. Practical logic requires attention to rules and "schemes" (X macros, configuration settings on the rules engine.) I wrote an adventure game with a few rooms and objects in Drools and dreamt of making something like "Inform 7 for business rules".

[zozbot234]

> Commonsense reasoning involves a lot of "Alice thinks that Jane thinks that..." and "A was true until 12:30 this afternoon, now A is false".

These are both examples of modalities. From a formal point of view, description logics are special cases of multi-modal logics. The semantics of these can in turn be understood as computationally well-behaved restrictions of FOL, where the logical quantifiers are understood to range over so-called "possible worlds".

[j-pb]

The issue with the DL approach to FOL fragments is that the operator-subset approach is too coarse grained. We need something more finegrained that allowes for syntactic and semantic constraints over the specific interpretations and theories. An example of such an approach is stratified negation in datalog. DL would simply ban negation or recursion, but limiting the syntax of datalog programs allows for correct semantics while still allowing solutions for many interesting problems.

One of our running gags is: "Snomed might not be able to give you a diagnosis on why you are sick, or provide you with a treatment plan, but thanks to the power and efficiency of description logics it can tell you that you leg bone is connected to your hip bone and that both are bones 80 billion times per second."

[PaulHoule]

It is fun with snomed to track a blood vessel in the periphery all the way to the heart and back.