diff --git a/subprojects/docs/src/learn/language/classes.md b/subprojects/docs/src/learn/language/classes.md
deleted file mode 100644
index 7278dc352..000000000
--- a/subprojects/docs/src/learn/language/classes.md
+++ /dev/null
@@ -1,14 +0,0 @@
----
-SPDX-FileCopyrightText: 2024 The Refinery Authors
-SPDX-License-Identifier: EPL-2.0
-description: Metamodeling in Refinery
-sidebar_position: 0
----
-
-# Classes and references
-
-:::warning
-
-Under construction
-
-:::
diff --git a/subprojects/docs/src/learn/language/classes/ContainmentInstance.svg b/subprojects/docs/src/learn/language/classes/ContainmentInstance.svg
new file mode 100644
index 000000000..197f4b48c
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/ContainmentInstance.svg
@@ -0,0 +1,227 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/InvalidInstance.svg b/subprojects/docs/src/learn/language/classes/InvalidInstance.svg
new file mode 100644
index 000000000..fb9dd37de
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/InvalidInstance.svg
@@ -0,0 +1,20 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg b/subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg
new file mode 100644
index 000000000..b28c295a7
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg
@@ -0,0 +1,229 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg b/subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg
new file mode 100644
index 000000000..95ba8def7
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg
@@ -0,0 +1,29 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg b/subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg
new file mode 100644
index 000000000..cdf365f0b
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg
@@ -0,0 +1,38 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg b/subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg
new file mode 100644
index 000000000..56a4d956c
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg
@@ -0,0 +1,69 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg b/subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg
new file mode 100644
index 000000000..81ab4a0cb
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg
@@ -0,0 +1,24 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/ReferencesSimple.svg b/subprojects/docs/src/learn/language/classes/ReferencesSimple.svg
new file mode 100644
index 000000000..fac748159
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/ReferencesSimple.svg
@@ -0,0 +1,43 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/classes/index.md b/subprojects/docs/src/learn/language/classes/index.md
new file mode 100644
index 000000000..73108039c
--- /dev/null
+++ b/subprojects/docs/src/learn/language/classes/index.md
@@ -0,0 +1,212 @@
+---
+SPDX-FileCopyrightText: 2024 The Refinery Authors
+SPDX-License-Identifier: EPL-2.0
+description: Metamodeling in Refinery
+sidebar_position: 0
+---
+
+# Classes and references
+
+Refinery supports _metamodeling_ to describe the desired structure of generated models.
+
+The metamodeling facilities are inspired by object-oriented software and the [Eclipse Modeling Foundation](https://eclipse.dev/modeling/emf/) (EMF) Core, a lightweight framework for data models.
+The textual syntax in Refinery for defining metamodels is largely compatible with [Xcore](https://wiki.eclipse.org/Xcore), a textual syntax for EMF metamodels.
+
+## Classes
+
+Classes are declared with the `class` keyword.
+
+Like in many programming languages, class members are specified between curly braces `{}`.
+If a class has no members, the declaration may be terminated with a `.` instead.
+
+```refinery
+% Class with no members.
+class Region {}
+
+% Alternative syntax without curly braces.
+class State.
+```
+
+By default, a _new object_ is added to the partial model to represent the instances of a class.
+For example, the new objects `Region::new` and `State::new` represent potential instances of the classes `Region` and `State`, respectively:
+
+import NewObjectsSimple from './NewObjectsSimple.svg';
+
+
+
+As you can see, no new objects represent potential nodes that are instanceof of both `Region` and `State`.
+In fact, such instances are not permitted at all.
+Each node must the instance of a _single most-specific class:_
+
+import InvalidInstance from './InvalidInstance.svg';
+
+
+
+### Inheritance
+
+Like in object-oriented programming languages, classes may declare _superclasses_ with the `extends` keyword.
+The inheritance hierarchy may not contain any cycles (a class cannot be a superclass of itself), but _multiple inheritance_ is allowed.
+
+Classes that can't be instantiated directly (i.e., a subclass must be instantiated instead) can be marked with the `abstract` keyword.
+Such classes do not have a _new object,_ since there are no direct instances to represent.
+
+```refinery
+abstract class CompositeElement.
+class Region.
+abstract class Vertex.
+abstract class RegularState extends Vertex.
+class State extends RegularState, CompositeElement.
+```
+
+Notice that the new object `State::new` is an instance of `CompositeElement`, `Vertex`, `RegularState`, and `State` as well.
+
+import NewObjectsWithInheritance from './NewObjectsWithInheritance.svg';
+
+
+
+## References
+
+The graph structure of model generated by Refinery is determined by the _references_ of the metamodel, which will appear as labeled edges between nodes (class instances).
+
+References are declared as class members by providing the _target type,_ and optional _multiplicity,_ and the name of the reference:
+
+```refinery
+class Vertex.
+class Transition {
+ Vertex[1] source
+ Vertex[1] target
+}
+```
+
+import ReferencesSimple from './ReferencesSimple.svg';
+
+
+
+You may add the `refers` keyword for compatibility with [Xcore](https://wiki.eclipse.org/Xcore). The following specification is equivalent:
+
+```refinery
+class Vertex.
+class Transition {
+ refers Vertex[1] source
+ refers Vertex[1] target
+}
+```
+
+### Opposite constraints
+
+The `opposite` keywords specifies that two references are in an _opposite_ relationship, i.e., if one reference is present in a direction, the other must be present between the same nodes in the opposite direction.
+
+```
+class Vertex {
+ Transition[] outgoingTransition opposite source
+ Transition[] incomingTransition opposite target
+}
+class Transition {
+ Vertex[1] source opposite outgoingTransition
+ Vertex[1] target opposite incomingTransition
+}
+```
+
+import ReferencesOppositeInstance from './ReferencesOppositeInstance.svg';
+
+
+
+Opposites must be declared in pairs: it is a specification error to declare the `opposite` for one direction but not the other.
+
+Unlike in EMF, references that are the `opposite` of themselves are also supported.
+These must always be present in both directions between two nodes.
+Thus, they correspond to undirected graph edges.
+
+```refinery
+class Person {
+ Person[] friend opposite friend
+}
+```
+
+import ReferencesOppositeSelf from './ReferencesOppositeSelf.svg';
+
+
+
+### Multiplicity
+
+_Multiplicity constrains_ can be provided after the reference type in square braces.
+They specify how many _outgoing_ references should exist for any given instance of the class.
+
+:::info
+
+To control the number of _incoming_ references, add an `opposite` reference with multiplicity constraint.
+
+:::
+
+A multiplicity constraint is of the form `[n..m]`, where the non-negative integer `n` is the _lower_ bound of outgoing references,
+and `m` is a positive integer or `*` corresponding to the _upper_ bound of outgoing references.
+The value of `*` represent a reference with _unbounded_ upper multiplicity.
+
+If `n` = `m`, the shorter form `[n]` may be used.
+The bound `[0..*]` may be abbreviated as `[]`.
+If the multiplicity constraint is omitted, the bound `[0..1]` is assumed.
+
+---
+
+In the following model, the node `v1` satisfies all multiplicity constraints of `outgoingTransition`.
+The node `v2` violates the lower bound constraint, while `v3` violates the upper bound constraint.
+All `Transition` instances satisfy the multiplicity constrains associated with `source`.
+
+```refinery
+class Vertex {
+ Transition[2..3] outgoingTransition opposite source
+}
+class Transition {
+ Vertex[1] source opposite outgoingTransition
+}
+```
+
+import MultiplicityConstraintsInstance from './MultiplicityConstraintsInstance.svg';
+
+
+
+### Containment hierarchy
+
+To structure models and ensure their connectedness, Refinery supports _containment_ constraints.
+
+References may be marked as _containment_ references with the `contains` keyword.
+
+Classes that are the _target type_ of at least one _containment_ reference are considered `contained`.
+An instance of a `contained` class must have exactly 1 incoming containment reference.
+Instances of classes that are not `contained` must _not_ have any incoming containment references.
+
+Containment references have to form a _forest_, i.e., they must not contain any cycles.
+The _roots_ of the forest are instances of classes that are not `contained`, while `contained` classes for the internal nodes and leaves of the trees.
+
+Opposites of _containment_ references have to be marked with the `container` keyword.
+They must not specify any multiplicity constraint, since the multiplicity is already implied by the containment hierarchy.
+
+---
+
+In the following model, the instances of `Region` are the roots of the containment hierarchy.
+The classes `Vertex` are `Transition` are both considered `contained`.
+
+```refinery
+class Region {
+ contains Vertex[] vertices opposite region
+}
+
+class Vertex {
+ container Region region opposite vertices
+ contains Transition[] outgoingTransition opposite source
+ Transition[] incomingTransition opposite target
+}
+
+class Transition {
+ container Vertex source opposite outgoingTransition
+ Vertex[1] target opposite incomingTransition
+}
+```
+
+Containment edges are show with **thick** lines:
+
+import ContainmentInstance from './ContainmentInstance.svg';
+
+
+
+Containment edges form trees, while non-containment references, such as `target`, may point across the containment hierarchy.
diff --git a/subprojects/docs/src/learn/language/logic/AssertionsError.svg b/subprojects/docs/src/learn/language/logic/AssertionsError.svg
new file mode 100644
index 000000000..8ddc65f30
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/AssertionsError.svg
@@ -0,0 +1,20 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/logic/AssertionsExample.svg b/subprojects/docs/src/learn/language/logic/AssertionsExample.svg
new file mode 100644
index 000000000..26b3d1fff
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/AssertionsExample.svg
@@ -0,0 +1,99 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/logic/DefaultAssertions.svg b/subprojects/docs/src/learn/language/logic/DefaultAssertions.svg
new file mode 100644
index 000000000..2ab002bf5
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/DefaultAssertions.svg
@@ -0,0 +1,129 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/logic/MultiObjects.svg b/subprojects/docs/src/learn/language/logic/MultiObjects.svg
new file mode 100644
index 000000000..a52325755
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/MultiObjects.svg
@@ -0,0 +1,81 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/logic/ObjectScopes.svg b/subprojects/docs/src/learn/language/logic/ObjectScopes.svg
new file mode 100644
index 000000000..440dfb192
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/ObjectScopes.svg
@@ -0,0 +1,58 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg b/subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg
new file mode 100644
index 000000000..6f9880652
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg
@@ -0,0 +1,58 @@
+
+
\ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/logic/index.md b/subprojects/docs/src/learn/language/logic/index.md
new file mode 100644
index 000000000..21107d6b5
--- /dev/null
+++ b/subprojects/docs/src/learn/language/logic/index.md
@@ -0,0 +1,256 @@
+---
+SPDX-FileCopyrightText: 2024 The Refinery Authors
+SPDX-License-Identifier: EPL-2.0
+description: Four-valued logic abstraction
+sidebar_position: 1
+---
+
+# Partial modeling
+
+Refinery allow precisely expressing _unknown,_ _uncertain_ or even _contradictory_ information using [four-valued logic](https://en.wikipedia.org/wiki/Four-valued_logic#Belnap).
+During model generation, unknown aspects of the partial model get _refined_ into concrete (true or false) facts until the generated model is completed, or a contradiction is reached.
+
+The _Belnap--Dunn four-valued logic_ supports the following truth values:
+
+* `true` values correspond to facts known about the model, e.g., that a node is the instance of a given class or there is a reference between two nodes.
+* `false` values correspond to facts that are known not to hold, e.g., that a node is _not_ an instance of a given class or there is _no_ reference between two nodes.
+* `unknown` values express uncertain properties and design decisions yet to be made. During model refinement, `unknown` values are gradually replaced with `true` and `false` values until a consistent and concrete model is derived.
+* `error` values represent contradictions and validation failures in the model. One a model contains an error value, it can't be refined into a consistent model anymore.
+
+## Assertions
+
+_Assertions_ express facts about a partial model. An assertion is formed by a _symbol_ and an _argument list_ of _nodes_ in parentheses.
+Possible symbols include [classes](../classes/#classes), [references](../classes/#references), and [predicates](../predicates).
+Nodes appearing in the argument list are automatically added to the model.
+
+A _negative_ assertion with a `false` truth value is indicated by prefixing it with `!`.
+
+---
+
+Consider the following metamodel:
+
+```refinery
+class Region {
+ contains Vertex[] vertices
+}
+class Vertex.
+class State extends Vertex.
+```
+
+Along with the following set of assertions:
+
+```refinery
+Region(r1).
+Vertex(v1).
+Vertex(v2).
+!State(v2).
+vertices(r1, v1).
+vertices(r1, v2).
+!vertices(Region::new, v1).
+!vertices(Region::new, v2).
+```
+
+import AssertionsExample from './AssertionsExample.svg';
+
+
+
+It is `true` that `r1` is an instance of the class `Region`, while `v1` and `v2` are instances of the class `Vertex`.
+We also assert that `v2` is _not_ an instance of the class `State`, but it is unknown whether `v1` is an instance of the class `State`.
+Types that are `unknown` are shown in a lighter color and with an outlined icon.
+
+It is `true` that there is a `vertices` reference between `r1` and `v1`, as well as `r1` and `v2`, but there is no such reference from `Region::new` to the same vertices.
+As no information is provided, it is `unknown` whether `State::new` is a vertex of any `Region` instance.
+References that are `unknown` are shown in a lighter color and with a dashed line.
+
+### Propagation
+
+Refinery can automatically infer some facts about the partial model based on the provided assertions by information _propagation._
+The set of assertions in the [example above](#assertions) is equivalent to the following:
+
+```refinery
+vertices(r1, v1).
+vertices(r1, v2).
+!State(v2).
+```
+
+By the type constraints of the `vertices` reference, Refinery can infer that `r1` is a `Region` instance and `v1` and `v2` are `Vertex` instances.
+Since `State` is a subclass of `Vertex`, it is still unknown whether `v1` is a `State` instance,
+but `v2` is explicitly forbidden from being such by the negative assertion `!State(v2)`.
+We may omit `!vertices(Region::new, v1)` and `!vertices(Region::new, v2)`, since `v1` and `v2` may be a target of only one [containment](../classes/#containment-hierarchy) reference.
+
+Contradictory assertions lead to `error` values in the partial model:
+
+```refinery
+State(v1).
+!Vertex(v1).
+```
+
+import AssertionsError from './AssertionsError.svg';
+
+
+
+### Default assertions
+
+Assertions marked with the `default` keyword have _lower priority_ that other assertions.
+They may contain wildcard arguments `*` to specify information about _all_ nodes in the graph.
+However, they can be overridden by more specific assertions that are not marked with the `default` keyword.
+
+---
+
+To make sure that the reference `vertices` is `false` everywhere except where explicitly asserted, we may add a `default` assertion:
+
+```refinery
+default !vertices(*, *).
+vertices(r1, v1).
+vertices(r2, v2).
+vertices(r3, v3).
+?vertices(r1, State::new).
+```
+
+import DefaultAssertions from './DefaultAssertions.svg';
+
+
+
+We can prefix an assertion with `?` to explicitly assert that some fact about the partial model is `unknown`.
+This is useful for overriding negative `default` assertions.
+
+## Multi-objects
+
+The special symbols `exists` and `equals` control the _number of graph nodes_ represented by an object in a partial model.
+
+By default, `exists` is `true` for all objects.
+An object `o` with `?exists(o)` (i.e., `exists(o)` explicitly set to `unknown`) may be _removed_ from the partial model.
+Therefore, it represents _at least 0_ graph nodes.
+
+By default, `equals` is `true` for its _diagonal_, i.e., we have `equals(o, o)` for all object `o`.
+For off-diagonal pairs, i.e., `(p, q)` with `p` not equal to `q`, we always have `!equals(p, q)`: distinct objects can never be _merged._
+If we set a _diagonal_ entry to `unknown` by writing `?equals(o, o)`, the object `o` becomes a **multi-object:** it can be freely _split_ into multiple graph nodes.
+Therefore, multi-objects represent _possibly more than 1_ graph nodes.
+
+| `exists(o)` | `equals(o, o)` | Number of nodes | Description |
+|:-:|:-:|-:|:-|
+| `true` | `true` | `1` | graph node |
+| `unknown` | `true` | `0..1` | removable graph node |
+| `true` | `unknown` | `1..*` | multi-object |
+| `unknown` | `unknown` | `0..*` | removable multi-object |
+
+In the Refinery web UI, `?exists(o)` is represented with a _dashed_ border, while `?equals(o, o)`
+
+```refinery
+node(node).
+
+node(removable).
+?exists(removable).
+
+node(multi).
+?equals(multi, multi).
+
+node(removableMulti).
+?exists(removableMulti).
+?equals(removableMulti, removableMulti).
+```
+
+import MultiObjects from './MultiObjects.svg';
+
+
+
+import TuneIcon from '@material-icons/svg/svg/tune/baseline.svg';
+import LabelIcon from '@material-icons/svg/svg/label/baseline.svg';
+import LabelOutlineIcon from '@material-icons/svg/svg/label/outline.svg';
+
+:::info
+
+You may use the _filter panel_ icon in refinery to toggle the visibility of special symbols like `exists` and `equals`.
+You may either show _both true and unknown_ values or _just true_ values.
+The _object scopes_ toggle will also show the number of graph nodes represented by an object in square brackets after its name, like in the figure above.
+:::
+
+By default, a **new object** `C::new` is added for each non-`abstract` [class](../classes#classes) `C` with `?exists(C::new)` and `?equals(C::new, C::new)`.
+This multi-object represents all potential instances of the class.
+To assert that no new instances of `C` should be added to the generated model, you may write `!exists(C::new)`.
+
+You may use the `multi` keyword to quickly defined a (removable) multi-object:
+
+```
+mutlti removableMulti.
+% This is equivalent to:
+% ?exists(removableMulti).
+% ?equals(removableMulti, removableMulti).
+```
+
+## Type scopes
+
+_Type scopes_ offer finer-grained control over the number of graph nodes in the generated model (as represented by the multi-objects) that `exists` or `equals` assertions.
+
+A _type scope constraint_ is formed by a unary symbol (a [class](../classes/#classes) or a [predicate](../predicates) with a single parameter) and _scope range._
+Ranges have a form similar to [multiplicity constraints](../classes#multiplciity): a range `n..m` indicates a lower bound of `n` and an upper bound of `m`.
+While an upper bound of `*` indicates a possibly unbounded number of objects, generated models will always be finite.
+Like for multiplicity constraints, the case `n..n` can be abbreviated as `n`.
+
+The number of nodes in the generated model can be controlled using the `node` special symbol.
+For example, we may write the following to generate a model with at least 100 at and most 120 nodes:
+
+```refinery
+scope node = 100..200.
+```
+
+A `scope` declaration may prescribe type scope constraint for any number of symbols, separated by `,`.
+Multiple `scope` declarations are also permitted.
+Multiple ranges provided for the same symbol will be intersected, i.e., they influence the generated model simultaneously.
+
+In other words,
+```
+scope Region = 10, State = 80..120.
+scope State = 100..150.
+% Equivalent to:
+scope Region = 10, State = 100..120.
+```
+
+The _object scopes_ option in the _filter panel_ may help in exploring the effects of object scopes.
+
+---
+
+Consider the example
+
+```refinery
+class Region {
+ contains Vertex[] vertices
+}
+class Vertex.
+class State extends Vertex.
+scope node = 100..120, Vertex = 50..*.
+```
+
+import ObjectScopes from './ObjectScopes.svg';
+
+
+
+Notice that Refinery could determine that there can be no more than 70 `Region` instances in the generated model, since at least 50 of the `100..120` nodes in the model must be `Vertex` instances.
+However, since `State` is a subclass of `Vertex` (i.e., `State::new` is also an instance of `Vertex`), the range `50..*` is shared between both `Vertex::new` and `State::new`, resulting in both representing `0..120` nodes.
+Nevertheless, every generated model will obey the scope constraint exactly, i.e., will have between 100 and 120 node, at least 50 of which are `Vertex` instances.
+
+By providing more information, Refinery can determine more precise ranges for multi-objects.
+For example, we may strengthen the scope constraints as follows:
+
+```refinery
+scope node = 100..120, Vertex = 50..*, State = 20.
+```
+
+import StrongerObjectScopes from './StrongerObjectScopes.svg';
+
+
+
+### Incremental scopes
+
+We may specify an _incremental_ object scope with the `+=` operator to determine the number of new instances to be added to the model.
+This is only allowed for symbol that are classes with no subclasses, as it directly influences the number of nodes represented by the corresponding `::new` object.
+
+For example, to ensure that between 5 and 7 `State` instances are added to the model, we may write:
+
+```refinery
+State(s1).
+State(s2).
+scope State += 5..7.
+```
+
+Since `s1` and `s2` are also instances of the `State` class, the generated concrete model will have between 7 and 9 `State` instances altogether.