Human Reasoning

2013-11-08

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]

- Individuals / Objects
- Classes / Sets / Concepts
- Relations

- The semantic web, Web 3.0, RDF, OWL, OWL-DL, etc...

- Systematized Nomenclature Of Medicine Clinical Terms

Snomed CT är ett internationellt begreppssystem som syftar till att göra dokumentationen i vård och omsorg enhetlig, entydig och ändamålsenlig. [...] Målet är att Snomed CT ska användas inom vård och omsorg i hela landet. [Socialstyrelsen]

- Concept1 - Relation - Concept2
- Common Cold - causative agent - Virus
- \(\mathtt{CommonCold}(x) \rightarrow \exists y (\mathtt{causativeAgent}(x,y) \land \mathtt{Virus}(y))\)
- \(\mathtt{CommonCold} \sqsubseteq \exists \mathtt{causativeAgent}. \mathtt{Virus}\)
- Based on a description logic.
- Used in so called
*Clinical decision support system*(CDSS).

- 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"

- \(\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}\)

- 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) \}\)

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

- \(O \models \varphi\) if all models of \(O\) are models of \(\varphi\).
- \(\models \varphi\) if all models are models of \(\varphi\).

A concept \(C\) is

satisfiableif there is a model \(M\) such that \(C^M \neq \emptyset\).

\(C\) is satisfiable iff \(\not\models C \sqsubseteq \bot\).

- \(\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}\)

A

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

Sometimes we need the TBox to be *acyclic*:

An atomic concept \(A\)

directly usesan atomic concept \(B\) in \(O\) if \(B\) occurs in the right-hand side of any axiom with \(A\) on the left-hand side. The relationusesis then the transitive closure of the directly uses relation. \(O\) isacyclicif no atomic concept \(A\) uses \(A\).

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 theclosed world assumption. Not so in DL. DL is monotone.

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

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

ALC is multi modal logic K:

- \(\forall R\) translates to \(\Box_R\)
- \(\exists R\) translates to \(\Diamond_R\)
- \(\sqcup\) to \(\lor\)
- \(\sqcap\) to \(\land\)
- \(\lnot\) to \(\lnot\)

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

A medical doctor gets a recommended treatment relying on a medical ontology, such as SNOMED-CT. (safety)

Actually, it follows from SNOMED-CT that \(\mathtt{AmpOfFinger} \sqsubseteq \mathtt{AmpOfHand}\).

Whydoes an entailment \(O \models \varphi\) hold?

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

A justification of \(\varphi\) (wrt \(O\)) is a

minimalsubset \(I \subseteq O\) such that \(I \models \varphi\).

is a justification for \(\mathtt{RRated} \sqsubseteq \mathtt{Movie}\).

- \(\mathtt{RRated} \sqsubseteq \mathtt{Thriller}\)
- \(\mathtt{Thriller} \sqsubseteq \mathtt{Movie}\)

- \(\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}\)

is a justification for \(\mathtt{Person} \sqsubseteq \bot\).

[Horridge, Parsia, Sattler]

The definition rests on a notion of 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\).

- 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

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

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

Justification | Success rate | Model complexity | Proof length |
---|---|---|---|

1 | 57% | 654 | 11 |

2 | 57% | 703 | 14 |

3 | 29% | 675 | 18 |

Why can't we extract explanations *directly from the proofs*?

These slides were made using: