[ontolog-forum] Ontologies vs Theories / Axioms vs Rules

[Peter Yim <peter.yim@xxxxxxxx>]

I'm relocating this very interesting thread from the [oor-forum] which started yesterday over here - ref. thread starting with message: http://ontolog.cim3.net/forum/oor-forum/2011-10/msg00008.html

I've made a best attempt to roll up the exchanges so far below.

... please continue the discussion on this forum.




----------
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Wed, Oct 19, 2011 at 9:07 AM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Bijan Parsia <bparsia@xxxxxxxxxxxx>
Cc: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>


Hi Bijan,

        [AH] Allow me to attempt re-phrasing what's been said. In contrast to a paradigm for ontologies like Cyc, whereby one tries to model the domain as faithfully and completely in one formalism and then delegates reasoning tasks based on the analysis of this expressive representation;

 

    [BP] Is that how Cyc works? That's not my understanding, but whatever :)

I over simplified and in fact cringed after reading the sent email. What I meant to contrast is that in many ways Cyc is an example of a paradigm which represents the domain in an expressive language and then finds the appropriate subsets that match decidable logics for reasoning. At least, that's my understanding. It uses a variety of reasoners.

    [BP] The problem with super expressive logics such as Common Logic is, roughly, the tool support sucks and probably sucks for the forseeable future.

I would hope that with the current work under way by the Bremen group (HeTS) and the Toronto group (COLORE), a CL ontology could be factored into more tractable fragments. Of course, not to mention a number of CL reasoners currently under development and the environment being developed by CameronRoss. Needless to say, I'm more optimistic about utilizing more expressive languages.

On Wed, Oct 19, 2011 at 11:42 AM, Bijan Parsia <bparsia@xxxxxxxxxxxx> wrote:

    In the end, it shouldn't really affect what you're trying to do. If you need to represent something, you need to represent it. If you put it in your "ontology" rather than in your "rule base", but the answers are the same, does it *really* matter?

Admittedly, the surface language might end up not mattering much, but I certainly was confused as to what people meant by Rule, and clarifications such as this thread can help avoid pointless future confusion when talking to different groups of people :D. Further, in the context of the OOR and using the OMV to tag various registered ontologies and create web-services and workflows around what is in the OOR, these distinctions could come to bear. 

Presumably, we're going to see more OWL+SWRL or RIF ontologies being deployed and registered in the repository. How will the SWRL or RIF modules be stored and what is the nature of their relationship (using OMV or an extension) to the OWL ontologies? What is the nature of a subset of some CL ontology that maps to some OWL+SWRL combo? And so on. To what extent can these mappings be automated and tools / services orchestrated to solve ontology related problems for reseachers / professionals?

Indeed, in the conference call earlier this week (http://ontolog.cim3.net/cgi-bin/wiki.pl?OOR/ConferenceCall_2011_10_18), I think there was a suggestion for rules should be stored externally(?). The sense I got was that not everyone involved in the discussion was clear about the distinction between rules / axioms, so it seems rather relevant.

Best,
Ali



_________________________________________________________________

----------
From: Bijan Parsia <bparsia@xxxxxxxxxxxx>
Date: Wed, Oct 19, 2011 at 8:42 AM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, Ali SH <asaegyn+out@xxxxxxxxx>


On 19 Oct 2011, at 16:20, Ali SH wrote:
> Dear Pat and Bijan,
>
> On Tue, Oct 18, 2011 at 6:52 PM, Pat Hayes <phayes@xxxxxxx> 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. The textbook terminology of formal logic has not been used in the applied ontology world for about the last two decades.)
>
> Thank you for your discussion and clarification, it's been very helpful! 
> Allow me to attempt re-phrasing what's been said. In contrast to a paradigm for ontologies like Cyc, whereby one tries to model the domain as faithfully and completely in one formalism and then delegates reasoning tasks based on the analysis of this expressive representation;

Is that how Cyc works? That's not my understanding, but whatever :)

> in this context we have more of a bottom-up, a priori engineered approach?

No?

> Before you begin your representation, you partition your domain into different types of knowledge and use a variety of representation / rule languages to capture different parts of intuitions. Simplifying greatly, does this fairly capture the essence of the paradigm?

Not for me.

I'd put it this way in both cases: You pick your language based on a variety of factors, most likely what your overly-enthusiastic friend forces on you, then do the best you can with the toolset available. With a formalism like OWL, we've made a basic tradeoff of expressivity in favor of computability (plus some other choices to improve usability). So, we have a nice set of tools that work rather well and an expanding suite of services (cf recent work on explanation or module extraction/dependency analysis). Our problem is that we have to work around expressivity limitations. A danger is that our world view becomes warped to those limitations.

The problem with super expressive logics such as Common Logic is, roughly, the tool support sucks and probably sucks for the forseeable future. (FOL reasoners are superawesome, but I still can't get a simple formalization of the Allan calculus in terms of "meets" to verify before o before -> before! The usual line I get from by FOL ATP peeps is "So, what decidable fragment does it fall into.) The advantage is, of course, expressivity (which can be a disadvantage, too, of course): You can say what you need to say, mostly, and usually rather directly. The problem is that you can't do much with it or check it very well. If you do use tools you often end up having to warp your representation to those tools. (Cf Rieter's Knowledge In Action for a very clever and systematic way of doing it...most of the time it's not so nice.)

Pick your poison :)

> All this said, I'm still a touch flummoxed at being able to adequately and consistently distinguish an axiom from a rule. For example, the standard inheritance / subclass relation of:
>
>     (forall (x) (if (dog x) (animal x)))
>
> is supported by virtually all DL's. It seems like it could be a rule to me.

In logics with a deduction theorem (or subsets there of) the distinction isn't big.

> I mean, Pellet or Racer would be able to use the class structure in an OWL-DL ontology to tell me that the properties of Animals apply to Dogs.

But they use a refutation mechanism, not "triggering" the rule.

In the end, I don't think the distinction in a general sense is worth getting all as worked up about it as many rule folks do. Just consider the particular formalism you are dealing with, note the syntax and semantics and how the commonly used proof procedures work, and move on. That it's a "RULE" language or *not* a rule language is, well, meh. Or, rather, mostly ideological.

>
>     [PH] 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; 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.. 

> and

>     [BP] No as true anymore [re inference rules]. "Consequence" based reasoning is becoming more popular esp. in restricted fragments such as EL, e.g.,

> Given these two statements, and putting aside the sociological issues for a moment, in this case, one can determine whether something is a "rule" really only in the context of the expressivity of a particular representation language? Roughly, anything that can't be represented in the formalism is considered a rule?

That would make rule langauges odd.

The simple rule of thumb is the union of horn clauses with implicitly univerisally quantified explicit variables (usually with variables bound to names) or IF-THEN productiony conditions is a rule. Everything else is not. Some non rules are equivalent to some rules.

> I.e. say I want to represent a fragment of law, I can only decide what is a rule by first deciding which formalism and reasoner I'm using, then anything that couldn't be expressed in said language is a candidate for a rule? 

Or you could just not care. That its a rule in some generalized sense is really quite pointless. That it can be expressed in the formalism that you want to use is important.

> In summary, what one means by a rule is wholly dependent on what representation language one deploys?

No, my summary is: Don't get hung up on this bit of terminology. It's not remotely helpful.

> Other people I've spoken to suggest that there is fundamentally something distinct about the notion of a rule from what should be contained in an ontology, which seems like a different issue altogether?

They are wrong.

>  They suggest that "concepts and rules" should be treated separately. 

This seems to be, at best, at a different level of conceptualization than the formalism.

> The description provided by Pat seem more to do with engineering, while those in the previous sentences hinge on a particular interpretation of ontology. 

Yeah, I wouldn't get hung up on what an "ontology" is either. Yet Another Rathole.

In the end, it shouldn't really affect what you're trying to do. If you need to represent something, you need to represent it. If you put it in your "ontology" rather than in your "rule base", but the answers are the same, does it *really* matter?

Cheers,
Bijan.


_________________________________________________________________

----------
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Wed, Oct 19, 2011 at 8:20 AM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Pat Hayes <phayes@xxxxxxx>
Cc: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>


Dear Pat and Bijan,


On Tue, Oct 18, 2011 at 6:52 PM, Pat Hayes <phayes@xxxxxxx> 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. The textbook terminology of formal logic has not been used in the applied ontology world for about the last two decades.)

Thank you for your discussion and clarification, it's been very helpful! 

Allow me to attempt re-phrasing what's been said. In contrast to a paradigm for ontologies like Cyc, whereby one tries to model the domain as faithfully and completely in one formalism and then delegates reasoning tasks based on the analysis of this expressive representation; in this context we have more of a bottom-up, a priori engineered approach? Before you begin your representation, you partition your domain into different types of knowledge and use a variety of representation / rule languages to capture different parts of intuitions. Simplifying greatly, does this fairly capture the essence of the paradigm?

All this said, I'm still a touch flummoxed at being able to adequately and consistently distinguish an axiom from a rule. For example, the standard inheritance / subclass relation of:

    (forall (x) (if (dog x) (animal x)))

is supported by virtually all DL's. It seems like it could be a rule to me. I mean, Pellet or Racer would be able to use the class structure in an OWL-DL ontology to tell me that the properties of Animals apply to Dogs.

    [PH] 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; 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.. 

and

    [BP] No as true anymore [re inference rules]. "Consequence" based reasoning is becoming more popular esp. in restricted fragments such as EL, e.g.,

Given these two statements, and putting aside the sociological issues for a moment, in this case, one can determine whether something is a "rule" really only in the context of the expressivity of a particular representation language? Roughly, anything that can't be represented in the formalism is considered a rule? I.e. say I want to represent a fragment of law, I can only decide what is a rule by first deciding which formalism and reasoner I'm using, then anything that couldn't be expressed in said language is a candidate for a rule? 

In summary, what one means by a rule is wholly dependent on what representation language one deploys?

Other people I've spoken to suggest that there is fundamentally something distinct about the notion of a rule from what should be contained in an ontology, which seems like a different issue altogether? They suggest that "concepts and rules" should be treated separately. The description provided by Pat seem more to do with engineering, while those in the previous sentences hinge on a particular interpretation of ontology. 

Thanks,
Ali


_________________________________________________________________

----------
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Wed, Oct 19, 2011 at 2:22 AM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Pat Hayes <phayes@xxxxxxx>
Cc: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, Ali SH <asaegyn+out@xxxxxxxxx>


On Oct 19, 2011, at 12:52 AM, 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'.

Pat, I believe I adapted my terminology quite precisely to the people I was trying to communicate with, namely, Ali and interested observers. :-) My purpose was nothing grander than to note the ambiguity of "rule" in the sense he was talking about and the use of "rule" in logic. As I noted in my post:

> The senses of "rule" you describe for the most part seem rather different.


That said, your lengthy discourse (with Bijan's qualifications) was very informative.

-chris


_________________________________________________________________

----------
From: Kathryn B Laskey <klaskey@xxxxxxx>
Date: Tue, Oct 18, 2011 at 6:11 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>


Well said. Thanks -- i was planning to write something similar but am too swamped to get to it.

On Oct 18, 2011, at 6:52 PM, Pat Hayes wrote:

> Guys, you have to adapt your terminology to the people you are trying to communicate with. ...[snip]...

_________________________________________________________________

----------
From: Bijan Parsia <bparsia@xxxxxxxxxxxx>
Date: Tue, Oct 18, 2011 at 5:12 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Pat Hayes <phayes@xxxxxxx>
Cc: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, Ali SH <asaegyn+out@xxxxxxxxx>


On 19 Oct 2011, at 00:59, Pat Hayes wrote:

> Bijans quibbles are all quite correct,

Indeed! :)

> but I plead that I was trying to get across a basic almost sociological divide here (and was talking to logicians) and there wasnt time to go into too much detail.

Sure. Just amending where I thought some more detail would help. Tastes vary.

And you are definitely on the side of angels at the moment (ducks).

> He is also quite right that OWL2 refers to "axioms", a fact I had simply forgotten. Its unusual, though, in this respect. Calling them axioms is by no means, um, axiomatic.

Indeed. But I think it's winning :) In rdf land, "triples" is by far preferred for many of the same reasons.

> One counter-quibble:

For what do we live, but to make quibble fodder for our neighbours, and quibble at them in our turn?

> On Oct 18, 2011, at 6:34 PM, Bijan Parsia wrote:
>
>> On 18 Oct 2011, at 23:52, Pat Hayes wrote:
>>
>> .....
>> [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".
>
> Well, that is a very natural way to see it from a logically trained POV, I agree. But the sense I often get is that this not in fact how implementers see it, but more like using a rule engine to do quick patch-around hacks to overcome a local lack of expressivity (eg doing a very quick check for transitivity)

This isn't my sense, qua implementor and friend of implementors, *except* maybe for OWLRL and languages/implementations like that. AL-log explicitly used a hybrid method, but while Pellet's rule support used a Rete it was *inside* the tableau (and worked *on* the completion graph). KAON2 reduced *everything* (DL axioms and DL Safe rules alike) to disjunctive datalog KBs. HermiT's hypertableau naturally incorporates horn kbs.

There is no "quick" check for transitivity in *class expressions*, of course. But over the named individuals and their relations to each other it is faster to do datalogish reasoning, for obvious reasons. I don't know of any OWL engine that does that, though.

> but not even claiming any kind of completeness or attempting to relate the rules to the logical semantics in other than a superficial way. I dont accuse you or your colleagues of such sloppiness, of course, nor do I mean to say that more careful or theoretically sound work is not done; but there are certainly more, um, shall we say, scruffy points of view which just want to get things working as quickly as possible.

Right, but my suggestion, sociologically, is that is more "from below" than "from above", i.e., going from a rule based implementation of RDFS to "some useful bit of OWL". These implementations are, of course, not hybrid either, but purely rule based.

> And my point in the email was only that Ali might well have come across some discussion from within that more engineering-oriented kind of tradition, is all.

No worries ;)

>> 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).
>
> Quite. I was talking about the bolting-together approach.

Yes, this is the point of clarification. The bolting together is really quite rare nowadays (though, interesting, current Pellet + Stardog the rdf store have some of this): If you have a DL engine with rules, it's as likely to be designed for rules (due to Boris Motik, mostly). If you don't, you likely just have a rules engine with some random axiomitzation of some fragment of OWL.

(Or you're in the polynomial DL space, where the two approachs coincide, really.)

Cheers,
Bijan.

_________________________________________________________________

----------
From: Pat Hayes <phayes@xxxxxxx>
Date: Tue, Oct 18, 2011 at 4:59 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, Bijan Parsia <bparsia@xxxxxxxxxxxx>
Cc: Ali SH <asaegyn+out@xxxxxxxxx>


Bijans quibbles are all quite correct, but I plead that I was trying to get across a basic almost sociological divide here (and was talking to logicians) and there wasnt time to go into too much detail. He is also quite right that OWL2 refers to "axioms", a fact I had simply forgotten. Its unusual, though, in this respect. Calling them axioms is by no means, um, axiomatic.

One counter-quibble:

On Oct 18, 2011, at 6:34 PM, Bijan Parsia wrote:

> On 18 Oct 2011, at 23:52, Pat Hayes wrote:
>
> .....
> [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".

Well, that is a very natural way to see it from a logically trained POV, I agree. But the sense I often get is that this not in fact how implementers see it, but more like using a rule engine to do quick patch-around hacks to overcome a local lack of expressivity (eg doing a very quick check for transitivity) but not even claiming any kind of completeness or attempting to relate the rules to the logical semantics in other than a superficial way. I dont accuse you or your colleagues of such sloppiness, of course, nor do I mean to say that more careful or theoretically sound work is not done; but there are certainly more, um, shall we say, scruffy points of view which just want to get things working as quickly as possible. And my point in the email was only that Ali might well have come across some discussion from within that more engineering-oriented kind of tradition, is all.

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

Quite. I was talking about the bolting-together approach.

Pat


>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/oor-forum/
> Subscribe: mailto:oor-forum-join@xxxxxxxxxxxxxxxx
> Config/Unsubscribe: http://ontolog.cim3.net/mailman/listinfo/oor-forum/
> Shared Files: http://ontolog.cim3.net/file/work/OOR/
> Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OpenOntologyRepository

------------------------------------------------------------
IHMC                                     (850)434 8903 or (650)494 3973
40 South Alcaniz St.           (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (850)291 0667   mobile
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes


_________________________________________________________________

----------
From: Bijan Parsia <bparsia@xxxxxxxxxxxx>
Date: Tue, Oct 18, 2011 at 4:34 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>
Cc: Ali SH <asaegyn+out@xxxxxxxxx>


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.

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

http://www.w3.org/TR/owl2-syntax/#Introduction

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.

http://www.w3.org/TR/owl2-syntax/#Axioms

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. 

Unless you quote the spec :)

Cheers,
Bijan.


_________________________________________________________________

----------
From: Pat Hayes <phayes@xxxxxxx>
Date: Tue, Oct 18, 2011 at 3:52 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, Ali SH <asaegyn+out@xxxxxxxxx>


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. The textbook terminology of formal logic has not been used in the applied ontology world for about the last two decades.)

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. 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), which operate by chaining together 'rules' (basically, and oversimplifying, Horn clauses thought of as encoding forward-constrained implications). 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.)

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, 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, and its paradigmatic tableaux reasoners achieve completeness within this decidable sub case. (There is a big theoretical literature recording the history and logical ramifications of all this, with links to modal logics and a great deal of advanced model theory.) The rule language tradition is far less logically based and more pragmatic: it typically pays no attention at all to completeness ( OK, I know there are exceptions, but they are achieved only by warping the semantics) and often thinks of the rule languages as more like programming languages than logics.

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, without sacrificing the guarantees of decideability provided by the use of the DL fragment to do the basic consistency chacking which supports practical ontology entailment. Such hybrids have been being proposed, implemented and used since the beginning of the semantic web effort.

I think this is what the sources cited by Ali are referring to. S

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

Pat Hayes

_________________________________________________________________

----------
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Tue, Oct 18, 2011 at 1:41 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Christopher Menzel <cmenzel@xxxxxxxx>
Cc: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>




On Tue, Oct 18, 2011 at 4:16 PM, Christopher Menzel <cmenzel@xxxxxxxx> wrote:

    On Oct 18, 2011, at 10:06 PM, Ali SH wrote:
    > Dear Leo and Chris,
    >
    > Thanks for the responses. I understand the distinction between an inference rule and an axiom,

    Right, as I'd suspected (and so noted at the bottom of my post).

Noted, but not acknowledged in my initial email response :D. 


    > the issue for me stems from a terminological confusion, because obviously, an axiom can express a rule (not in the same sense as an inference rule; i.e. if X is an employee then Y assigns X an employee number).

    Looks like an axiom to me. :-)  "Rule" just seems to have a pragmatic connotation that what is expressed is something that *ought* to be done by whoever is playing a certain role (Y, presumably, in this case). 

In the LKIF paper, they have statements such as:  

    This is well explained in Deliverable D1.1, where LKIF itself is discussed: for more complex or other types of knowledge than terminological knowledge we also need rule formalisms. (page 3 in [1])

    There are also several rule-based approaches that try to capture norms in rules with notions like violation or duty as antecedent or conclusion. The rule itself captures the meaning of the norm, so that the confusion between norm and normative statementis again retained. (page 35 in [1])

Which suggests to me that they aren't referring to inference rules. But I have no clue how to reliably distinguish a rule from an axiom. In  [2] http://www.estrellaproject.org/doc/D1.1-LKIF-Specification.pdf, they have a section describing their rules, which seems to me to be a mix of axioms and inference rules.

For example, these seem like axioms to me (page 74 in [2]):

    (rule §-9-306-1
    (if (and (goods ?s ?c)
    (consideration ?s ?p)
    (collateral ?si ?c)
    (collateral ?si ?p)
    (holds (perfected ?si ?c) ?e)
    (unless (applies §-9-306-3-2 (perfected ?si ?p))))
    (holds (perfected ?si ?c) ?e)))
    (rule §-9-306-2a
    (if (and (goods ?t ?c)
    (collateral ?s ?c))
    (not (terminates ?t (security-interest ?s)))))
    (fact F1 (not (terminates T1 (security-interest S1))))
    (fact F2 (collateral S1 C1))

 


    > That said, your interpretation of rule poses an interesting question, do people distinguish an ontology from an ontology + whatever inference rules used to interpret it?

    Inference rules simply come packaged with whatever logic one is building one's ontology on (or affixing one's ontology axioms to).

That's what I thought.
 


    > Based on analogy then, does gmail as software refer to the gmail the source code, or gmail the compiled, deployed code?

    Sorry, man, that's too heavy for me! :-)

I have a feeling this question has been tread before.... ;) 


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

    It seems to me that (a) and (b) are two viable meanings for "ontology".  (c) does not seem feasible to me, except insofar as one identifies a reasoner with the logic it is based on.

This is where I guess the analogy with traditional software breaks down. Gmail compiled and deployed seems to me to be (c). Though for ontologies, the line between (b) and (c) are a bit unclear to me. I don't know how someone (i.e. human) would be able to actually access / generate (b) without some reasoner (their mind?).

[1] Joost Breuker, Rinke Hoekstra, Alexander Boer, Kasper van den Berg, Rossella Rubino, Giovanni Sartor, Monica Palmirani, Adam Wyner, and Trevor Bench-Capon. OWL ontology of basic legal concepts (LKIF-Core). Deliverable 1.4, Estrella, 2007.

[2] Alexander Boer, Marcello Di Bello, Kasper van den Ber, Tom Gordon, Andr´as F¨orh´ecz, R´eka Vas. Specification of the Legal Knowledge Interchange Format. Deliverable 1.1, Estrella, 2007

Best,
Ali
-- 


(•`'·.¸(`'·.¸(•)¸.·'´)¸.·'´•) .,.,


_________________________________________________________________

----------
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, Oct 18, 2011 at 1:16 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Ali SH <asaegyn+out@xxxxxxxxx>
Cc: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>


On Oct 18, 2011, at 10:06 PM, Ali SH wrote:
> Dear Leo and Chris,
>
> Thanks for the responses. I understand the distinction between an inference rule and an axiom,

Right, as I'd suspected (and so noted at the bottom of my post).

> the issue for me stems from a terminological confusion, because obviously, an axiom can express a rule (not in the same sense as an inference rule; i.e. if X is an employee then Y assigns X an employee number).

Looks like an axiom to me. :-)  "Rule" just seems to have a pragmatic connotation that what is expressed is something that *ought* to be done by whoever is playing a certain role (Y, presumably, in this case).

> That said, your interpretation of rule poses an interesting question, do people distinguish an ontology from an ontology + whatever inference rules used to interpret it?

Inference rules simply come packaged with whatever logic one is building one's ontology on (or affixing one's ontology axioms to).

> Based on analogy then, does gmail as software refer to the gmail the source code, or gmail the compiled, deployed code?

Sorry, man, that's too heavy for me! :-)

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

It seems to me that (a) and (b) are two viable meanings for "ontology".  (c) does not seem feasible to me, except insofar as one identifies a reasoner with the logic it is based on.

-chris


_________________________________________________________________

----------
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Tue, Oct 18, 2011 at 1:06 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, "Obrst, Leo J." <lobrst@xxxxxxxxx>, Christopher Menzel <cmenzel@xxxxxxxx>


Dear Leo and Chris,
Thanks for the responses. I understand the distinction between an inference rule and an axiom, the issue for me stems from a terminological confusion, because obviously, an axiom can express a rule (not in the same sense as an inference rule; i.e. if X is an employee then Y assigns X an employee number).
That said, your interpretation of rule poses an interesting question, do people distinguish an ontology from an ontology + whatever inference rules used to interpret it? Based on analogy then, does gmail as software refer to the gmail the source code, or gmail the compiled, deployed code? 
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)?
I'd be curious to hear from Todd (or others who distinguish between ontologies with and without rules) which sense of rule they refer to. In my conversations with people, I don't believe they are referring to "inference rule" when they distinguish between ontologies as not having rules and some system that also has rules.
When people say that X doesn't have rules, do they mean that it can't express something like (from wiki on RIF)

        IF MARRIED(?x, ?y) THEN LOVES(?x, ?y)

or that the processing of the rule isn't part of the ontology?
Thanks,
Ali

_________________________________________________________________

----------
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, Oct 18, 2011 at 12:38 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>


On Oct 18, 2011, at 8:50 PM, Ali SH wrote:
> Hello Michael and all,
> I noticed some confusion today during the telecon when Michael and Todd were talking about differences between Ontologies & Theories, and Rules & Axioms. I've actually encountered a number of people who make this distinction -- that an ontology doesn't really express "rules", and that these rules are somehow different from "axioms". The line is still blurry to me, but it seems to be that in this terminology, a "rule" refers to anything that OWL doesn't support, whereas in the CL (and FOL world) there is no distinction between these "rules" and "axioms".

In logic, "rule" typically means "rule of inference". Together with some set of logical axioms, rules are an essential part of a logical system like propositional or first order logic. Thus, a standard set of logical axiom (schemas) for propositional logic are:

(φ → (ψ → φ)
((φ → (ψ → θ)) → ((φ → ψ) → (φ → θ))
(¬φ → ψ) → ((¬φ → ¬ψ) → φ)

Note, however, that with axioms alone you are powerless to do anything more than write down axioms. Rules of inference define a notion of one sentence following from other and, hence, enables the derivation of theorems that are not axioms.  The usual rule of inference for propositional logic, of course, is modus ponens:

MP: ψ follows from φ and φ → ψ.

A proof of propositional logic, then, is any sequence of sentences such that each sentence is either an axiom or follows from sentences occurring earlier in the sequence.

Predicate logic simply adds axioms for quantification, e.g.,

∀αφ → φ(τ), where τ is an "acceptable" instance of φ
∀α(φ → ψ) → (φ → ∀αφ), where α does not occur free in φ

and, optionally, identity, and (typically) adds a rule of inference for universal generalization:

UG: ∀αφ follows from φ. (Note this is usually qualified in certain ways but never mind.)

CL, for better or worse, does not specify a proof theory but, if it did, this is surely (?) what "rule" would mean.  The senses of "rule" you describe for the most part seem rather different. In my experience, these "non-logical" uses of "rule" are usually synonymous with "non-logical axiom". Speaking of which:

A first-order theory (in some first-order language) is any set of non-logical axioms in the language of first-order logic.  Peano Arithmetic, Pat Hayes' ontology of liquids, etc are all first-order theories.

I have a feeling you already knew this stuff but maybe someone else will find it helpful.

-chris


_________________________________________________________________

----------
From: Obrst, Leo J. <lobrst@xxxxxxxxx>
Date: Tue, Oct 18, 2011 at 12:35 PM
Subject: Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>, Michael Gruninger <gruninger@xxxxxxxxxxxxxxx>


Ali and all,

 
Sorry I missed today, folks, just too busy these days.


I understand the notion of rule to be about the consequence relation, e.g., modus ponens. A, A -> B |- B (where |- is syntactic consequence; this is usually called entailment). This is at the meta-logic level. These are often called “inference rules”.

An axiom (typically) uses the base logical connectives, and in this case refers to (material) implication (conditional), e.g., (A /\ (A->B)) -> B. This is at the object (logic) level.

This is how I explain it to most of my students and others. Generally rule-based systems or inference engines will use generalized modus ponens, resolution, etc.

A deductive system can consist of axioms and inference rules, or axioms only, or inference rules only.

Most folks bandy these terms around, and don’t make a clear distinction between consequence and (material) implication. And you will get a lot of gruff grief from people.


Modus Ponens:

X ® Y
X
------
Y


That inference rule is actually equivalent to: ((X ®  Y) Ù X) ®  Y

X         Y         X® Y             ((X® Y) Ù X)            ((X ®  Y) Ù X) ®  Y
T          T          T                      T                                  T
T          F          F                      F                                  T
F          T          T                      F                                  T
F          F          T                      F                                  T


I have found the following to provide good descriptions (aside from the usual books introducing logic or its meta-theory):

Hunter, Geoffrey. 1973.  MetaLogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press.

Ryan, Mark; Martin Sadler.  1992.  Valuation Systems and Consequence Relations. In: Abramsky, S.; Gabbay, Dov; Maibaum, T.S.E. Handbook of Logic in Computer Science, Volume 1, Background: Mathematical Structures. Oxford: Clarendon Press, pp. 1-78.

Concerning the difference between ontologies and theories: a group of people will say that an ontology is just a logical theory, i.e., a theory expressed in a logic. Others, philosophically realist, will say that an ontology is a logical theory about some aspect of the real world. I prefer the latter.


Other points:

If you look at SWRL, it is really a kind of Horn Logic/Rule representation, i.e., a generalized Modus Ponens form used by logic programming. RIF contains many notions of “rules” not just this kind of “logical inference rule”, but production rules (forward-chaining rules) from expert systems, etc.


Thanks,

Leo

_________________________________________________________________

----------
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Tue, Oct 18, 2011 at 11:50 AM
Subject: [oor-forum] Ontologies vs Theories / Axioms vs Rules
To: Michael Gruninger <gruninger@xxxxxxxxxxxxxxx>, OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>


Hello Michael and all,

I noticed some confusion today during the telecon when Michael and Todd were talking about differences between Ontologies & Theories, and Rules & Axioms. I've actually encountered a number of people who make this distinction -- that an ontology doesn't really express "rules", and that these rules are somehow different from "axioms". The line is still blurry to me, but it seems to be that in this terminology, a "rule" refers to anything that OWL doesn't support, whereas in the CL (and FOL world) there is no distinction between these "rules" and "axioms".

An example of such a distinction can be found in documentation re the LKIF-Core (Legal Knowledge Interchange Format) ontology which makes claims such as [1] (http://www.estrellaproject.org/doc/D1.4-OWL-Ontology-of-Basic-Legal-Concepts.pdf):

    We adhere to a rather restrictive view on what an ontology should contain: terminological knowledge, i.e. intensional definitions of concepts, represented as classes with which we interpret (model) the world (page 7)

where things that would have other types of "rules" are part of "frameworks" and not included as part of the ontology. 

In these cases, it would still be possible to map from LKIF to a CL ontology, but the reverse would either lose information or require the selection LKIF and possibly one or more "frameworks" (perhaps stored as OWL + RIF or SWRL combos in OOR). That said, I'm not sure what the status of a RIF or SWRL module w/o an accompanying ontology would be in the context of OOR, and how one would represent these combinations using OMV. 

Further, in their discussion of the deontics surrounding law, they state:

    "Although the situation description may be expressed without problems as a framework cast in OWL-DL, but OWL-DL does not allow this deontic qualification to be expressed as a metaclass, or rather that the deontic qualification allows reified statements. There are three solutions to this problem. ... The second one is to express norms as rules, which has an intuitive appeal, as in common sense terms legal norms are synonymous with legal rules: one has to obey the rules. However, this does not immediately solve the tractability problem either as description logics and rule formalisms are not necessarily compatible (see also [Boer et al., 2007])." (page 9)

I'm not certainly how prevalent these distinction between ontology, theory, axiom and rules are, but I've come across it in (OWL heavy) literature, and it is unclear to me whether such distinctions are adequately covered by the OMV metadata. At the very least, if web services will be built around the OOR platform, then this is an issue that needs to be addressed.

Might someone help elucidate this distinction?

Best,
Ali

[1] Joost Breuker, Rinke Hoekstra, Alexander Boer, Kasper van den Berg, Rossella Rubino, Giovanni Sartor, Monica Palmirani, Adam Wyner, and Trevor Bench-Capon. OWL ontology of basic legal concepts (LKIF-Core). Deliverable 1.4, Estrella, 2007.
-- 


_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/oor-forum/
Subscribe: mailto:oor-forum-join@xxxxxxxxxxxxxxxx
Config/Unsubscribe: http://ontolog.cim3.net/mailman/listinfo/oor-forum/
Shared Files: http://ontolog.cim3.net/file/work/OOR/
Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OpenOntologyRepository

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)