Learning objectives
- Distinguish concepts (classes), roles (binary relationships) and individuals.
- Represent TBox axioms and ABox assertions using Description Logic notation.
- Distinguish asserted facts from logically entailed facts.
- Perform simple instance checking, instance retrieval and subsumption queries.
- Explain why failure to derive a fact does not establish its negation under the open-world assumption.
1 · The formal language
We use a small, explicitly defined fragment of ALC-style Description Logic. The lab supports atomic concept inclusions, the two role constraints below, concept assertions and role assertions. It is not a complete ALC reasoner.
Knowledge base
TBox \(\mathcal{T}\): general statements about concepts and roles.
ABox \(\mathcal{A}\): statements about named individuals.
Interpretation
A non-empty domain \(\Delta^\mathcal{I}\), together with an interpretation of every concept, role and individual name.
Syntax used in this laboratory
| Expression | Meaning | Example |
|---|---|---|
| \(C\sqsubseteq D\) | Every C is a D (concept inclusion) | \(Student\sqsubseteq Person\) |
| \(C(a)\) | Individual a is an instance of C | \(Student(Alice)\) |
| \(R(a,b)\) | a is related to b by role R | \(EnrolledIn(Alice,AI)\) |
| \(\exists R.\top\sqsubseteq C\) | Anything related by R to at least one thing is a C (domain constraint) | \(\exists EnrolledIn.\top\sqsubseteq Person\) |
| \(\top\sqsubseteq\forall R.C\) | Every R-successor is a C (range constraint) | \(\top\sqsubseteq\forall EnrolledIn.Course\) |
Semantics: the central satisfaction conditions
Here, \(C^\mathcal{I}\subseteq\Delta^\mathcal{I}\) and \(R^\mathcal{I}\subseteq\Delta^\mathcal{I}\times\Delta^\mathcal{I}\). The symbol \(\top\) denotes the whole domain.
2 · Start with a knowledge base
The initial TBox and ABox are shown below. Select a statement to see its role in the knowledge base.
The first two axioms define subclasses. The last two constrain the domain and range of EnrolledIn.
These statements concern named individuals.
3 · TELL — Add knowledge
Tell adds an axiom or assertion. Choose the statement type and enter its symbols. Names are case-sensitive.
Current knowledge base
4 · ASK — Query the knowledge base
Ask whether an assertion follows, retrieve instances of a concept, or test whether one concept is subsumed by another.
Inference trace
The trace distinguishes facts explicitly told from facts derived by the supported inference rules.
5 · Experiment: change one fact
Try the following sequence. Predict the result before clicking Ask.
- Tell
ResearchStudent ⊑ Student. - Tell
ResearchStudent(Bob). - Ask whether
Person(Bob)follows. - Tell
EnrolledIn(Bob, Robotics)as a role assertion. - Ask whether
Course(Robotics)follows. Explain which TBox axiom supports the result.
Lecturer(Bob), you cannot conclude ¬Lecturer(Bob). The information may simply be unknown.6 · Mathematical view of the queries
A knowledge base entails an assertion when that assertion is true in every model of the knowledge base.
For instance checking, the query is \(C(a)\). For subsumption, the query is \(C\sqsubseteq D\). For retrieval, the answer set is the named individuals a for which \(\mathcal{K}\models C(a)\).
What this implementation computes
The interactive engine computes closure for a finite, positive fragment: named concept assertions, named role assertions, atomic subclass inclusions, and the displayed domain/range constraints. It does not implement all ALC constructors, negation, disjointness, existential witness generation, equality, or a complete DL tableau procedure. Its positive entailment results are limited to the stated fragment.
7 · Check your understanding
Is Student ⊑ Person an ABox assertion?
No. It is a TBox axiom: it constrains the interpretation of the concepts.
If Student(Alice) and Student ⊑ Person, what follows?
Person(Alice) follows by applying the concept inclusion to Alice.
If Lecturer(Bob) is not derivable, is ¬Lecturer(Bob) true?
No. Under the open-world assumption, absence of evidence is not evidence of negation.