On 18 Oct 2011, at 23:52, Pat Hayes wrote:
Guys, you have to adapt your terminology to the people you are trying to communicate with. In the OWL/RDF/RIF/Semantic-Web/LInked-Data world, there is no such thing as an 'inference rule'. (If there were, it would be a line of code inside an inference engine; but most inference engines don't work that way in any case, but instead build tableaux.
No as true anymore. "Consequence" based reasoning is becoming more popular esp. in restricted fragments such as EL, e.g.,
Frantisek Simancik, Yevgeny Kazakov, Ian Horrocks: Consequence-Based Reasoning beyond Horn Ontologies. IJCAI 2011: 1093-1098
Yevgeny Kazakov, Markus Krötzsch, Frantisek Simancik: Unchain My EL Reasoner. Description Logics 2011
(KAON2 had a related technique applies to SHIQ kbs.
Plus, Tableaux (or tree methods) typically work by deriving logical consequences (i.e., representatives of models or contradictions).
The textbook terminology of formal logic has not been used in the applied ontology world for about the last two decades.)
Ehhhhh. The distinction between a inference rule and, more generally, a proof theory/procedure/system and an object sentence/axiom/wff is alive and well. Plenty of areas of formal logic tend not to focus on "inference rules" per se.
That is not what the people that Ali is citing are talking about. In the applied-semantic-web world, traditional logics are not widely used, in fact hardly at all. The most widely used formalisms are description logics; so widely used in fact that for many people, DL's simply *are* the 'language' for writing ontologies, and the very idea of an ontology written any anything other than a DL (except maybe something even less expressive, such as RDF) is not even contemplated or mentioned.
I quibble. As extensions to OWL are continually proposed, explored, and debated, it's really far too strong to say that alternatives are not on the horizon. Many modellers treat whatever language they know and have a tool for as exhaustive of the possibilities, but that's often true regardless of the language. OWL/RDF/RDFS, being rather popular, just mean that they loom larger on the horizon and modellers are not forced to contemplate alternatives.
However, this world does recognize another class of notations, loosely derived from Prolog or from production systems (which were developed entirely separately from logics and so share almost no scholarly or terminological links with the logic field),
I'll grant you production systems, but not Prolog. Programming with Logic, after all :) Plus the relationship between relational databases, datalog, and Prolog and first order logic are quite standardly discussed.
The main difference is less heterogeneity of basic proof procedure in the Prolog/Datalog world: Resolution is king in a way that it's not for even for FOL ATP anymore.
which operate by chaining together 'rules' (basically, and oversimplifying, Horn clauses thought of as encoding forward-constrained implications).
Since you lampshade the oversimplification, I forgive it :)
So there is a large and active field which develops, studies and categorizes "rule languages" which range in complexity from simple Horn-clause forward-inference engines to elaborate things with defaults, exceptions and so on. There is also a usage of "rule" as in 'business rule', and an active area of formalization and standardization for these 'rules' , in which they are seen as essentially deontic rules, encoding normative ways to behave rather than facts which are true or false. And these are still considered to be 'rules' and 'rule languages'. So it is not obvious that it all reduces to Horn clauses in every case. (Merging an assertional with a deontic language would be an interesting challenge.) And then there are logic-programming systems like Prolog, and production systems. All of these have a great deal in common at the implementation level, so they have come to be seen as parts of a single field of 'rule languages', one which now holds its own conferences, journals, standardization committees, etc.. etc..(For example, try googling RuleML.)
In expert systems, esp. deriving from production system, "inference rule" often means a domain specific encapsulation of a reasoning pattern such as the relation between a test result and the probabiltiy of a disease or metacognitive advice such as if the diagnosis confidence is low, perform another test. Indeed, any law likeish generalization, as opposed to concrete facts.
Both of these formalisms - description logics and rule languages - can be viewed as subcases of FOL (as indeed can relational DBases) and this point of view often seems obvious or trivial to logicians, but it is far from obvious in practice,
Actually, not even in theory. Finite (for datebases) and preferred/minimal model theory are both complex and have lots of profundity (e.g., descriptive complexity).
especially as these fields have developed rather different ways to be practically useful. DL restricts the logical expressivity to a decideable subset of FOL with the finite model property,
Quibble: Not quite. SHIQ et al do not have the finite model property per se (since its possible to encode structures with infinite descending chains, i.e., descendent relations). But they do have something which is called various things but basically that you have an associated structure which is finite (in SHIQ's case, basically, every infinite model becomes regular after a certain size, so cycle detection (called "Blocking") can ensure termination).
[snip]
Still, there has been widespread interest in extending the expressive power of a DL logic by adding some of the functionality of a rule language to it. This has the great appeal of keeping the DL fragment intact while allowing inference engines to step outside the DL world where needed,
Er...why isn't this just "They are more expressive logics". I'm not sure I see, from the generic inference engine POV, the difference between, e.g., adding transitivity to ALC and adding DL Safe rules. (Obviously, from an implementation perspective, they are quite different. Some are sometimes amenable some of the time to hybrid proof procedures, but those aren't even always preferred these days, at least, in the sense of bolting together separatedly developed engines).
[snip]
So, now, let us switch back to logical terminology, and I will put scare quotes around the earlier usages. Are 'rules' axioms? Yes, pretty much, if we are talking baout the Horn-clause style of rule;
Even in bog standard FOL, we can admit extended derived rules (e.g., by allowing a substitution rule onto theorems). As I recall from my intro to symbolic logic days, this is done in textbooks to reduce the size of the proof theory from a metalogical point of view while still allowing a reasonably convenient proof system. (Plus progressive exercises: Proof double negation using modus pones and indirect proof or whatnot).
although there are 'rule' languages which allow one to say things that cannot be said in normal logics, eg default assumptions, negation-by-failure, closed-world presumptions, etc.. However, that terminology of 'axiom' would be anathematic in the ontology world.
OWL 2 ontologies consist of the following three different syntactic categories:....
Axioms are statements that are asserted to be true in the domain being described. For example, using a subclass axiom, one can state that the class a:Student is a subclass of the class a:Person.
Etc.
Worse, and my bad, we all now use them for entailments, i.e., "Entailed axiom". Oh well.
It smacks of mathematics (which ontology engineering most definitely is not) and it carries the presumption of being an 'assumed truth', which again is inappropriate in this other world. It would be much better to say, statement or _expression_ or sentence, rather than axiom.
My experience, which let me to write that above bit, is that people found "statement" and "sentence" confusing because it *wasn't* distinct enough. "Axiom" is more like "line of code": the difference helps keep clear what we're talking about (and prevents people from thinking they understand when they don't). YMMV.
But yes, many 'rules' are sentences, in fact sentences of the form ((A and B and C) imply D), where A--D are atomic sentences.
When people refer to an ontology (or an ontology artifact), are they referring singularly to (a) the axioms, or (b) the axioms under deductive > closure, or (c) the axioms in combination(s) with reasoner(s)?
In the OWL/RDF world, definitely (a). However, don't call them 'axioms', please.
Bijan.