First page
Back
Continue
Last page
Graphics
Take a very simple
case
-
Define the type Ex :
-
- the terms are “classes” (A, B, …) and
“individuals” (a, b, …)
- there are two possible relationships between classes:
-
- “subclassing” i.e., A ⊑ B, B ⊑ C,
etc., and
- “equivalence”, i.e. A ≣ B
- there is one relationship combining individuals to classes:
“typing” i.e. a:A, b:A,…
-
An example for a universe: the vocabulary: {a, A,
B} with the axioms {a:A, A ⊑
B}
-
The goal is to define a semantics so that we could
infer
a:B