Quick Start

Write your first Relatum program in under a minute.

1. Create a Cell

The app opens with the Workspace tab. Double-click an example or workspace file to open it, or create a new file with + File.

2. Write a Program

<element> a, b, c

<rel> equiv/2 : equivalence

equiv(a, b)
equiv(b, c)

derive

3. Run

Click Run All or press Ctrl+Enter in a cell. The output appears below each cell showing:

• Declarations and auto-generated rules
• Initial facts
• Derived facts (highlighted in green)
• Summary: rounds, total facts, saturation status

4. Experiment

Add more cells, try different properties, write custom rules. Each cell executes independently and contributes to a shared knowledge base.

Elements

The atoms of your universe.

Everything in Relatum is an element. Elements are declared by placing them inside a container using angle-bracket syntax.

Syntax

# Declare elements in the root container
<element> a, b, c

# Declare elements, then use them as types
<element> Person, City
<Person> alice, bob, carol
<City> paris, london

The Root: <element>

Every declared element automatically belongs to element. Writing <element> a, b, c is the simplest way to introduce elements.

Elements as Types

Any element can be used as a type (container), but it must be declared first. When you write <Person> alice, bob:

1. Person must already exist as an element.
2. alice and bob are declared as elements belonging to Person.

<element> Animal, Cat
<Animal> Cat, Dog
<Cat> whiskers, mittens

Membership Constrains Relations

When a relation declares a signature like <rel> R/2 : Person, City, only elements in Person can appear in argument 1, and only elements in City in argument 2. This applies to both user-written and derived facts.

Relations

Named connections between terms.

A relation is a named predicate with a fixed arity. equiv/2 is binary; between/3 is ternary.

Syntax

<rel> equiv/2                          # plain relation
<rel> equiv/2 : equivalence              # with properties
<rel> lt/2 : reflexive, transitive       # multiple properties
<rel> lives_in/2 : Person, City         # membership constraints
<rel> friend/2 : Person, Person, symmetric # membership + properties

Properties

Facts

Ground atoms — the initial knowledge base.

A fact is a ground instance of a relation. All terms must be declared constants (or compound terms).

Syntax

equiv(a, b)
lt(x, y)
between(a, b, c)

Validation

• The relation must be declared with <rel>.
• The number of terms must match the arity.
• Every term must be a declared constant or compound term.
• Membership constraints are checked for each argument position.

Rules

Inference rules for deriving new facts.

Rules express: "if these premises hold, derive these conclusions." They drive forward-chaining inference.

Syntax

<rule> name: premises |- conclusions

Premises and conclusions are comma-separated atoms. Variables are prefixed with ?.

Examples

# Symmetry
<rule> sym: R(?x, ?y) |- R(?y, ?x)

# Transitivity
<rule> trans: R(?x, ?y), R(?y, ?z) |- R(?x, ?z)

# Cross-relation
<rule> f2k: friend(?x, ?y) |- knows(?x, ?y)

# Multi-conclusion
<rule> both: eq(?x, ?y) |- leq(?x, ?y), leq(?y, ?x)

How Variables Work

• Variables (?x, ?y) are pattern wildcards matching any constant.
• Same variable in multiple positions requires same constant.
• The engine finds all satisfying substitutions, then instantiates conclusions.
• Only fully-bound conclusions become new facts.

Compound Terms

Structured terms and Skolem witnesses.

Beyond simple atoms, Relatum supports compound terms — function-like structures that create new terms from existing ones.

Syntax

# Compound term in a fact
group_op(a, inv(a), identity)

# Compound term in a rule (Skolem witness)
<rule> has_inv: member(?x) |- group_op(?x, inv(?x), identity)

A compound term is written as name(arg1, arg2, ...) where each argument can itself be a term (atom, variable, or another compound).

Skolem Witnesses

When a compound term appears in a rule conclusion with a variable, it creates a Skolem witness — a new structured term that depends on the matched variable. For example, inv(?x) in a conclusion creates a unique inverse for each element.

Depth Limit

Compound terms can nest: inv(inv(a)), inv(inv(inv(a))), etc. To prevent infinite nesting, use the depth directive:

depth 3    # max nesting depth for compound terms

The default depth is 5. Any derived fact containing a term deeper than this limit is silently dropped.

Use Cases

• Group theory: inv(?x) as inverse, op(?x, ?y) as multiplication
• Successor arithmetic: s(zero), s(s(zero))
• Structured data: pair(?x, ?y), cons(?h, ?t)

Derive & Prove

Commands to compute closure and query provenance.

derive

The derive command triggers the closure engine, applying all rules until saturation or a limit.

derive          # default: up to 100 rounds
derive 10       # limit to 10 rounds

What Happens During Derive

Each round, the engine:

1. Applies all rules (auto-generated + user-defined) to current facts
2. Generates reflexive facts for reflexive relations
3. Applies congruence for congruent relations
4. Checks for new facts

Stops when: saturated (no new facts), round limit reached, or fact limit (10,000) exceeded.

prove

The prove command queries the provenance of a specific fact — how it was derived.

prove equiv(a, c)

Output shows the derivation tree: which rule fired and which premises were used, recursively back to user-declared facts.

depth

The depth directive sets the maximum nesting depth for compound terms.

depth 3

Must appear before derive. Default is 5.

Algorithm

How the closure engine works internally.

Forward Chaining

Relatum uses semi-naive forward chaining, similar to Datalog evaluation. Starting from initial facts, it repeatedly applies rules until a fixed point.

Round Structure

for each round:
  1. Rule application
     for each rule:
       find all substitutions matching premises
       instantiate conclusions
       add new ground facts

  2. Reflexivity
     for each reflexive relation R:
       for each constant t: add R(t, t)

  3. Congruence
     for each congruent relation R:
       for each R(a, b) where a != b:
         for each fact S(...a...): add S(...b...)

  4. Fixed-point check
     if no new facts: STOP (saturated)

Complexity

• Single-premise rules: O(|rules| × |facts|) per round
• Multi-premise rules: O(|facts|^|premises|) worst case
• Congruence: O(|pairs| × |facts|) per round

Relation Properties

What each property does under the hood.

Reflexive

For every constant t in the universe, adds R(t, t) before rule application. Respects membership constraints.

Symmetric

Auto-generates rule R(?x, ?y) |- R(?y, ?x).

Transitive

Auto-generates rule R(?x, ?y), R(?y, ?z) |- R(?x, ?z). Two-premise join on ?y.

Congruent

If R(a, b) holds and S(..., a, ...) exists, derives S(..., b, ...). Propagates equivalence through the entire fact base.

Equivalence = All Four

: equivalence is shorthand for : reflexive, symmetric, transitive, congruent.

Safety & Limits

Guarding against infinite derivation.

Built-in Limits

When Limits Are Hit

The engine stops and reports the current state. Output shows capped instead of saturated. Derived facts are valid but incomplete.

Tips

• Start with few constants and add gradually.
• Use derive 5 to limit rounds while experimenting.
• Use depth 2 to limit Skolem term nesting.
• Be cautious with transitive + many constants.

Cells & Execution

The notebook execution model.

Cell Types

The notebook has two cell types:

• Code cells: contain Relatum DSL programs. Executed by the closure engine.
• Markdown cells: rich text notes using Markdown syntax.

Per-Cell Execution

Each code cell runs independently. Click the play button on a cell or press Ctrl+Enter while editing to execute just that cell. Run All executes all code cells in order.

Cumulative Knowledge Base

All cells share a single knowledge base. When you execute a cell, its declarations and facts are added to the global KB. The status bar shows total facts, derived count, and rounds.

Cell Operations

Hover over a cell to reveal the floating toolbar:

• ↑ / ↓ — move cell up/down
• code / md — convert between code and markdown
• × — delete cell

Use + code or + markdown buttons between cells or at the bottom to add new cells.

Undo

Press Ctrl+Z when not focused in any editor to undo the last cell operation (add, delete, move, convert). Each tab has its own undo stack (up to 30 levels).

Markdown Cells

Rich text annotations for your notebook.

Creating Markdown Cells

Click + markdown to add a markdown cell, or use the toolbar to convert an existing code cell.

Editing & Preview

Click a markdown cell to enter edit mode. Click outside or press Escape to render the preview. Supported syntax:

• # Heading, ## Subheading, ### Sub-subheading
• **bold**, *italic*, `inline code`
• - unordered list, 1. ordered list
• ```code blocks```
• [link text](url)
• > blockquote

Knowledge Base Panel

Explore and manage the accumulated knowledge base.

Opening the Panel

Click the KB button in the status bar, or click the panel header at the bottom of the screen.

Contents

The KB panel shows all accumulated state across all executed cells:

• Elements: all declared constants and containers
• Relations: declared relation schemas with arities and properties
• Rules: both user-defined and auto-generated rules
• Facts: initial + derived facts

Search

Use the search box at the top of the KB panel to filter items. Search matches against element names, relation names, rule names, and fact contents.

Retraction

Click the × next to any KB item to retract it. Retracted items appear crossed out and are excluded from future derivations. Click the + to restore a retracted item.

Use Clear All to reset the entire knowledge base.

Tabs & Files

Multi-tab workflow and file management.

Multiple Tabs

Each tab is an independent notebook with its own cells, knowledge base, undo stack, and execution state. Click a tab to switch; click × to close it.

Creating Files

In the Workspace tab, click + File to create a new notebook. Focus a folder first to create inside it.

Opening Files

Double-click any file in the Workspace or Examples section to open it in a new tab.

Saving Files

Click Save in the header to save the current tab to the workspace. The file contains:

• All cells (code and markdown) with their source text
• Cell output HTML (for code cells that have been executed)

The file does not save the knowledge base state, execution order, or retraction state — these are recomputed by re-running cells.

.relnb Format

{
  "version": 1,
  "cells": [
    { "type": "code", "source": "..." },
    { "type": "md", "source": "# Title" },
    { "type": "code", "source": "...", "output": "<html>" }
  ]
}

Editor Features

Syntax highlighting, autocomplete, and more.

Syntax Highlighting

Code cells have live syntax highlighting with the following color scheme:

Autocomplete

As you type in a code cell, an autocomplete dropdown appears with context-aware suggestions:

• Keywords: <element>, <ele>, <rel>, <relation>, <rule>, derive, prove, depth
• Declared elements: all constants from <element> / <Container>
• Declared relations: relation names with arity
• Declared rules: rule names

Navigate with ↑ / ↓ arrow keys, accept with Tab or Enter, dismiss with Escape.

Output Search

After executing a cell, use the search box in the output area to filter results. Matching text is highlighted.

Example: Equivalence Closure

The canonical Relatum example.

<element> a, b, c

<rel> equiv/2 : equivalence

equiv(a, b)
equiv(b, c)

derive

What the engine derives

• Symmetry: equiv(b, a), equiv(c, b)
• Transitivity: equiv(a, c)
• Symmetry of derived: equiv(c, a)
• Reflexivity: equiv(a, a), equiv(b, b), equiv(c, c)

Saturates in 2-3 rounds with 9 total facts (complete 3×3 equivalence class).

Example: Partial Order

Reflexive + transitive, but NOT symmetric.

<element> a, b, c, d

<rel> leq/2 : reflexive, transitive

leq(a, b)
leq(b, c)
leq(c, d)

derive

What the engine derives

• Reflexivity: leq(a, a), leq(b, b), leq(c, c), leq(d, d)
• Transitivity: leq(a, c), leq(a, d), leq(b, d)

leq(b, a) is not derived because the relation is not symmetric.

Example: Custom Rules

User-defined inference beyond built-in properties.

<element> alice, bob, carol

<rel> friend/2 : symmetric
<rel> knows/2

<rule> f2k: friend(?x, ?y) |- knows(?x, ?y)
<rule> knows_trans: knows(?x, ?y), knows(?y, ?z) |- knows(?x, ?z)

friend(alice, bob)
friend(bob, carol)

derive

Derivation chain

1. Symmetry: friend(bob, alice), friend(carol, bob)
2. f2k: knows(alice, bob), knows(bob, carol), ...
3. knows_trans: knows(alice, carol), knows(carol, alice), ...

Everyone ends up knowing everyone.

Example: Congruence

How congruence propagates equivalence through other relations.

<element> a, b, c

<rel> equiv/2 : equivalence
<rel> R/2

equiv(a, b)
R(a, c)

derive

What congruence does

Because equiv is congruent and equiv(a, b) holds, the engine sees R(a, c) and substitutes a → b, deriving R(b, c).

Example: Membership

Restricting which elements each relation argument accepts.

<element> Person, City
<Person> alice, bob, carol
<City> paris, london

<rel> lives_in/2 : Person, City
<rel> friend/2 : Person, Person, symmetric
<rel> same_city/2 : City, City, equivalence

lives_in(alice, paris)
lives_in(bob, paris)
lives_in(carol, london)

<rule> shared: lives_in(?x, ?c), lives_in(?y, ?c) |- same_city(?c, ?c)

derive

What happens

• Membership prevents nonsense: lives_in(paris, alice) would be rejected.
• Reflexivity respects membership: same_city(t, t) only for cities.
• Rules are membership-filtered: derived facts violating constraints are dropped.

Grammar Reference

Complete syntax of the Relatum DSL.

Lexical Elements

Statements

# Element declaration (root container)
<element> name1, name2, ...
<ele> name1, name2, ...          # shorthand

# Relation declaration (container for relation names)
<relation> name1, name2, ...
<rel> name1, name2, ...           # shorthand

# Typed element declaration (Container must be declared first)
<Container> member1, member2, ...

# Relation schema declaration
<rel> name/arity
<rel> name/arity : property1, property2, ...
<rel> name/arity : Container1, Container2, ...
<relation> name/arity : Container1, Container2, property, ...

# Rule declaration
<rule> name: atom1, atom2, ... |- atom3, atom4, ...

# Fact (ground atom)
name(term1, term2, ...)

# Commands
derive
derive N
prove name(term1, term2, ...)
depth N

Properties

Terms

A term is one of:

• A constant identifier: a, alice, zero
• A variable: ?x, ?name (in rules only)
• A compound: f(term, ...), e.g. inv(?x), s(zero)

Keyboard Shortcuts

Quick keys for the notebook interface.