Ontology

An ontology is a specification of a conceptualization. That is, an ontology is a description (like a formal specification of a program) of the concepts and relationships that can exist for an agent or a community of agents. [...] My colleagues and I have been designing ontologies for the purpose of enabling knowledge sharing and reuse. [Gruber, 1992]

SNOMED-CT

• Systematized Nomenclature Of Medicine Clinical Terms

Syntax

ALC - Attributive Concept Language with Complement

• The set of concepts is built up from atomic concepts \(A\) and roles \(R\): \[C ::=A \mathbin\vert \top \mathbin\vert \bot \mathbin\vert \lnot C \mathbin\vert C \sqcup C \mathbin\vert C \sqcap C \mathbin\vert \exists R.C \mathbin\vert \forall R.C\] where \(A\) is an atomic concept and \(R\) a role.
• The set of formulas is defined by: \[ \varphi ::= C \equiv C \mathbin\vert C \sqsubseteq C \mathbin\vert C \] where \(C\) is a concept.
• No individual variables!
• \(\exists R. C\) "All things with an \(R\)-successor in \(C\)". "R some C"
• \(\forall R. C\) "All things with all \(R\)-successors in \(C\)". "R all C"

Examples

• \(\mathtt{Male} \sqsubseteq \mathtt{Person}\)
• \(\exists \mathtt{hasChild}.\mathtt{Male}\)
• \(\forall \mathtt{hasChild}.\mathtt{Male}\)
• \(\exists \mathtt{hasChild}.\mathtt{Male} \sqcap \forall \mathtt{hasChild}.\mathtt{Male}\)

Semantics

• A model \(M\) gives an interpretation to each atomic concept and role.
• By a recursive definition each concept \(C\) is given an interpretation \(C^M \subseteq M\).
• \(\top^M = M\) and \(\bot^M = \emptyset\)
• \((C \sqcup D)^M = C^M \cup D^M\).
• \((C \sqcap D)^M = C^M \cap D^M\).
• \((\lnot C)^M = M \setminus C^M\).
• \((\forall R.C)^M = \{a \in M | \forall x \in M (\langle a,x\rangle \in R^M \rightarrow x \in C^M) \}\)
• \((\exists R.C)^M = \{a \in M | \exists x \in M (\langle a,x\rangle \in R^M \land x \in C^M) \}\)

Semantics continued

• \(M \models C \sqsubseteq D\) iff \(C^M \subseteq D^M\).
• \(M \models C \equiv D\) iff \(C^M = D^M\).

Examples

• \(\mathtt{Person} \sqsubseteq \lnot\mathtt{Movie}\)
• \(\mathtt{RRated} \sqsubseteq \mathtt{Movie}\)
• \(\mathtt{RRated} \equiv \mathtt{Thriller} \sqcup (\forall \mathtt{hasViolenceLevel}.\mathtt{High})\)
• \(\exists \mathtt{hasViolenceLevel}.\top \sqsubseteq \mathtt{Movie}\)

Terminology Box

A TBox is a set \(O\) of formulas of the form \(A \equiv D\) or \(A \sqsubseteq D\) where \(A\) is an atomic concept and each atomic concept occurs at most once on the left hand side of a formula in \(O\).

Assertion Box

An ABox consists of assertions of the form \(C(a)\) and \(R(a,b)\) where \(a\) and \(b\) are constants.

• Not included in our simplified system.

• An ABox is, in some sense, equivalent to a relational database where we only allow unary and binary relations.

Important: In the context of relational databases we have the closed world assumption. Not so in DL. DL is monotone.

• A pair of a TBox and an ABox is called a Knowledge Base.

First-order Logic

• Clearly any concept can be rewritten as a formula with a free variable.

\(\forall R_1. (C \sqcap \exists R_2 .C)\) is translated to \[\forall y (R_1(x,y) \rightarrow (C(y) \land \exists z (R_2(y,z) \land C(z))))\]

• ALC translates in this way into a small fragment of FOL.
• ALC can be translated into FO². (Sat is NEXPTIME)
• ALC can be translated into GF.

Modal propositional logic

Complexity

Description Logic Complexity Navigator

Intro

An engineer developing an ontology \(O\) suddenly realizes that \(O \models \top \sqsubseteq \bot\). (debugging)

Proofs

• Several proof system for DL.
• Usually based on tableaux systems. (Not very surprising, remember ALC `is' multi modal K.)
• These systems are constructed to get fast automatic theorem provers (called reasoners in the DL-community).
• They are not well suited as explanations for humans.

Justifications

A justification of \(\varphi\) (wrt \(O\)) is a minimal subset \(I \subseteq O\) such that \(I \models \varphi\).

• \(\mathtt{Person} \sqsubseteq \lnot\mathtt{Movie}\)
• \(\mathtt{RRated} \sqsubseteq \mathtt{Movie}\)
• \(\mathtt{RRated} \equiv \mathtt{Thriller} \sqcup (\forall \mathtt{hasViolenceLevel}.\mathtt{High})\)
• \(\exists \mathtt{hasViolenceLevel}.\top \sqsubseteq \mathtt{Movie}\)

Lemmatized justifications

[Horridge, Parsia, Sattler]

Complexity measure

• What is the complexity of an entailment \(I \models \varphi\)?
• We want to model cognitive complexity.
• The naïve approach of Horridge et al:

The complexity of an entailment \(I \models \varphi\) is the sum of a number of complexity scores.

The complexity scores are syntactic and semantic scores such as:

• 100 times the number of axiom types in \(I,\varphi\).
• 10 times the number of constructors in \(I,\varphi\).

A better way

• Use a natural proof system somehow based on a cognitive model.
• Define the complexity of an entailment as the length of the shortest proof.
• The proof system should be:
  • Linear
  • Local
  • Deep

A natural proof system

• Rules, for example:
• Axioms, such as: \(C \sqcup \lnot C \sqsubseteq \top\)
• Cognitive Restrictions that correspond to bounded working memory.

An example proof

Results

• A procedure for finding the shortest proof was implemented in Haskell by Abdul Rahim Nizamani.
• A small experiment was reported on in the Horridge et al paper. 14 participants.

But hey!

These slides were made using:

• reveal.js
• pandoc
• mathjax