Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules

[Ali SH <asaegyn+out@xxxxxxxxx>]

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

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

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

_________________________________________________________________
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/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     (01)