Fix a few bugs in the GUI

Cargo.toml

@@ -26,6 +26,27 @@ proptest = "1.4"  # property-based testing
 rand = "0.9.2"
 tempfile = "3.10" # temp dirs for persistence tests
 
+[features]
+default = []
+gui = ["eframe", "egui_extras", "rfd"]
+
+[dependencies.eframe]
+version = "0.29"
+optional = true
+
+[dependencies.egui_extras]
+version = "0.29"
+optional = true
+
+[dependencies.rfd]
+version = "0.15"
+optional = true
+
 [[bin]]
 name = "geolog"
 path = "src/bin/geolog.rs"
+
+[[bin]]
+name = "geolog-gui"
+path = "src/bin/geolog-gui.rs"
+required-features = ["gui"]

README2.md

@@ -0,0 +1,274 @@
+# Geolog Development Notes
+
+This document describes the features and components added to the geolog project (by me, Hassan).
+
+## Overview
+
+Geolog is a language for geometric logic - a type theory with semantics in topoi and geometric morphisms, designed as a unified language for database schemas, queries, and migrations.
+
+## Components
+
+### Core Components (Pre-existing)
+
+- **Parser & Lexer** (`src/lexer.rs`, `src/parser.rs`) - Chumsky-based parser for geolog syntax
+- **AST** (`src/ast.rs`) - Abstract syntax tree representation
+- **Core Types** (`src/core.rs`) - Signatures, structures, theories, axioms
+- **Elaboration** (`src/elaborate.rs`) - Type checking and elaboration
+- **Store** (`src/store.rs`) - Append-only persistent storage with version control
+- **REPL** (`src/repl.rs`) - Interactive command-line environment
+- **Solver** (`src/solver.rs`) - Model enumeration for geometric theories
+- **Query Engine** (`src/query/`) - Relational algebra backend for queries
+- **Chase Algorithm** (`src/query/chase.rs`) - Fixpoint computation for axiom closure
+
+### Debugger (`src/debugger.rs`)
+
+Interactive debugger for the chase algorithm providing:
+- Step-through execution
+- Breakpoints on axiom name patterns
+- Variable inspection
+- Iteration stepping
+
+Usage in REPL:
+```
+:debug-chase <instance> [max_iterations]
+```
+
+### GUI Application (`src/gui/`)
+
+A full-featured graphical interface built with egui.
+
+#### Building the GUI
+
+```bash
+# Build with GUI feature
+cargo build --features gui
+
+# Run the GUI
+cargo run --features gui --bin geolog-gui
+
+# With workspace persistence
+cargo run --features gui --bin geolog-gui -- -d ./myproject
+
+# Load a file on startup
+cargo run --features gui --bin geolog-gui -- examples/preorder.geolog
+```
+
+#### GUI Architecture
+
+```
+src/gui/
+├── mod.rs                    # Module exports
+├── app.rs                    # Main GeologApp (egui::App implementation)
+├── state.rs                  # GuiState wrapping ReplState
+├── panels/
+│   ├── mod.rs
+│   ├── browser.rs            # Theory/instance tree browser
+│   ├── editor.rs             # Code editor with line numbers
+│   ├── inspector.rs          # Detail view for selected items
+│   └── console.rs            # Output/error messages
+└── visualizations/
+    ├── mod.rs
+    ├── chase.rs              # Chase step-through visualization
+    └── graph.rs              # Relation graph visualization
+```
+
+#### GUI Features
+
+**Browser Panel (Left)**
+- Tree view of all theories and instances
+- Filter/search functionality
+- Click to select, right-click for context menu
+- Shows counts (sorts, functions, relations, axioms, elements)
+
+**Editor Panel (Center Top)**
+- Multi-line code editor
+- Line numbers
+- Run button (or Ctrl+Enter) to execute code
+- Clear button
+
+**Inspector Panel (Center Bottom)**
+- Theory details: parameters, sorts, functions, relations, instance fields, axioms
+- Instance details: elements by sort, function values, relation tuples, nested instances
+- Collapsible sections
+- "View Graph" button for instances
+
+**Console Panel (Bottom)**
+- Scrollable message log
+- Color-coded messages: info (gray), success (green), error (red), warning (orange)
+- Auto-scroll option
+- Clear button
+- **Integrated REPL input** with command history (Up/Down arrows)
+  - Type `:help` for commands
+  - Type `:list` to list theories/instances
+  - Type `:inspect <name>` to inspect
+  - Type `:chase <instance>` to run chase
+  - Or type geolog code directly
+
+**Adjustable Panels**
+- Browser panel (left): drag right edge to resize
+- Console panel (bottom): drag top edge to resize
+- Editor/Inspector split: drag the separator bar between them
+
+**Chase Visualization**
+- Step/Run All/Stop controls
+- Events log showing axiom firings with bindings
+- Breakpoint management
+- Current structure info (elements, relation tuples)
+- Mode indicator (Idle/Stepping/Running/Completed)
+
+**Graph Visualization**
+- Nodes represent elements (colored by sort)
+- Edges represent relation tuples
+- Interactive: drag nodes, zoom (scroll), pan
+- Relation filter dropdown
+- Reset Layout / Fit buttons
+- Hover to see sort name
+
+#### UI Layout
+
+```
+┌─────────────────────────────────────────────────────────────┐
+│  File   Edit   View   Chase   Help                          │
+├────────────┬────────────────────────────────────────────────┤
+│ ▼ Theories │  ┌─────────────────────────────────────────┐   │
+│   Preorder │  │ Editor                                  │   │
+│   Graph    │  │ theory Foo {                            │   │
+│ ▼ Instances│  │   X : Sort;                             │   │
+│   Chain3   │  │ }                     [Run] [Clear]     │   │
+│            │  ├─────────────────────────────────────────┤   │
+│            │  │ ═══════════ [drag to resize] ═══════════│   │
+│            │  ├─────────────────────────────────────────┤   │
+│            │  │ Inspector: Chain3 : Preorder            │   │
+│            │  │ ▼ Elements (3)                          │   │
+│            │  │   X: bot, mid, top                      │   │
+│            │  │ ▼ Relations                             │   │
+│            │  │   leq: 6 tuples [View Graph]            │   │
+│            │  └─────────────────────────────────────────┘   │
+├────────────┴────────────────────────────────────────────────┤
+│ Console                                              [Clear]│
+│ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms)  │
+│ + Defined instance Chain3 : Preorder (3 elements)          │
+│─────────────────────────────────────────────────────────────│
+│ geolog> :list                                         [Run] │
+└─────────────────────────────────────────────────────────────┘
+```
+
+## CLI Commands
+
+### REPL Commands
+
+```
+:help [topic]              Show help (topics: syntax, examples)
+:quit                      Exit the REPL
+:list [target]             List theories/instances
+:inspect <name>            Show details of a theory or instance
+:source <file>             Load and execute a geolog file
+:clear                     Clear the screen
+:reset                     Reset all state
+
+# Version Control
+:commit [msg]              Commit current changes
+:history                   Show commit history
+
+# Instance Mutation
+:add <inst> <elem> <sort>  Add element to instance
+:assert <inst> <rel> args  Assert relation tuple
+:retract <inst> <elem>     Retract element
+
+# Query
+:query <inst> <sort>       List all elements of a sort
+:explain <inst> <sort>     Show query execution plan
+:compile <inst> <sort>     Show RelAlgIR compilation
+:chase <inst> [max_iter]   Run chase on instance axioms
+:debug-chase <inst> [max]  Run chase with interactive debugger
+
+# Solver
+:solve <theory> [budget]   Find model of theory from scratch
+:extend <inst> <theory>    Find extension of instance to theory
+```
+
+### CLI Usage
+
+```bash
+# Start REPL (in-memory)
+cargo run
+
+# Start REPL with workspace persistence
+cargo run -- -d ./myproject
+
+# Load file on startup
+cargo run -- examples/preorder.geolog
+
+# Show help
+cargo run -- --help
+```
+
+## Dependencies
+
+### Core Dependencies
+- `chumsky` - Parser combinators
+- `ariadne` - Error reporting
+- `uuid` - Unique identifiers
+- `rkyv` - Zero-copy serialization
+- `rustyline` - Readline for REPL
+- `indexmap` - Ordered hash maps
+
+### GUI Dependencies (feature = "gui")
+- `eframe` - egui framework with native window
+- `egui_extras` - Additional egui widgets
+- `rfd` - Native file dialogs
+
+## Example
+
+```geolog
+// Define a preorder theory
+theory Preorder {
+  X : Sort;
+
+  // The ordering relation: x <= y
+  leq : [x: X, y: X] -> Prop;
+
+  // Reflexivity: x <= x
+  ax/refl : forall x : X.
+    |- [x: x, y: x] leq;
+
+  // Transitivity: x <= y and y <= z implies x <= z
+  ax/trans : forall x : X, y : X, z : X.
+    [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
+}
+
+// Define an instance with automatic chase
+// The 'chase' keyword applies axioms to compute the closure
+instance Chain3 : Preorder = chase {
+  bot : X;
+  mid : X;
+  top : X;
+
+  // Assert the basic ordering; chase derives reflexive pairs
+  // and transitive closure (bot <= top)
+  [x: bot, y: mid] leq;
+  [x: mid, y: top] leq;
+}
+```
+
+After loading this file, the chase algorithm automatically computes:
+- Reflexive pairs: `bot <= bot`, `mid <= mid`, `top <= top`
+- Transitive closure: `bot <= top`
+
+You can also define an instance without `chase` and run `:chase Chain3` manually.
+
+## Development
+
+```bash
+# Check without GUI
+cargo check
+
+# Check with GUI
+cargo check --features gui
+
+# Run tests
+cargo test
+
+# Build release
+cargo build --release --features gui
+```

notes/001-architecture.md

@@ -0,0 +1,151 @@
+# Architecture
+
+## What Geolog Is
+
+Geolog is a command-line tool for defining rules and automatically deriving facts from them. Think of it like a spreadsheet that can figure out new cells based on formulas you define, except the "formulas" are logical rules and the "cells" are facts about things.
+
+**Example:** You tell Geolog "if A is friends with B, and B is friends with C, then A knows C." Then you say "Alice is friends with Bob" and "Bob is friends with Charlie." Geolog automatically figures out "Alice knows Charlie."
+
+---
+
+## Tech Stack
+
+**Language:** Rust (2021 edition)
+
+### Key Dependencies
+
+| Crate               | What It Does                                                    |
+|---------------------|-----------------------------------------------------------------|
+| `chumsky`           | Reads `.geolog` files and understands their structure           |
+| `ariadne`           | Shows helpful error messages with line numbers                  |
+| `rkyv`              | Saves data to disk efficiently                                  |
+| `rustyline`         | Makes the interactive prompt work (arrow keys, history, etc.)   |
+| `egglog-union-find` | Tracks when two things are actually the same thing              |
+| `roaring`           | Stores large sets of numbers efficiently                        |
+| `indexmap`          | Hash maps that remember insertion order                         |
+| `memmap2`           | Reads files by mapping them directly into memory                |
+
+### Testing Tools
+
+| Tool | Purpose |
+|------|---------|
+| `insta` | Compares output against saved "snapshots" to catch regressions |
+| `proptest` | Generates random inputs to find edge cases |
+| `tempfile` | Creates temporary directories for tests |
+
+---
+
+## How Data Flows Through the System
+
+```
+┌─────────────────────────────────────────────────────┐
+│                    USER INTERFACE                    │
+│  You type commands or load .geolog files here        │
+├─────────────────────────────────────────────────────┤
+│                   PARSING LAYER                      │
+│  Turns text into a structured tree (like HTML DOM)   │
+│  Example: "P : Sort;" becomes {name: "P", kind: Sort}│
+├─────────────────────────────────────────────────────┤
+│                 ELABORATION LAYER                    │
+│  Checks types and resolves names                     │
+│  Example: Verifies "src : E -> V" refers to real     │
+│           sorts E and V that were declared           │
+├─────────────────────────────────────────────────────┤
+│                    CORE LAYER                        │
+│  The verified, type-checked representation           │
+│  Everything here is guaranteed to be well-formed     │
+├─────────────────────────────────────────────────────┤
+│                  STORAGE LAYER                       │
+│  Saves everything to disk, tracks history            │
+│  Like git for your data                              │
+├─────────────────────────────────────────────────────┤
+│               QUERY & SOLVER LAYER                   │
+│  Runs the chase algorithm to derive new facts        │
+│  Searches for models that satisfy your rules         │
+├─────────────────────────────────────────────────────┤
+│                  TENSOR ALGEBRA                      │
+│  Efficiently checks which rules need to fire         │
+│  Uses sparse matrices for performance                │
+└─────────────────────────────────────────────────────┘
+```
+
+---
+
+## Directory Structure
+
+| Path                | What's There |
+|---------------------|--------------|
+| `src/bin/geolog.rs` | The main program entry point — run `cargo run` and this executes |
+| `src/lib.rs`        | Library code that other Rust programs could use |
+| `src/repl.rs`       | The interactive prompt (handles `:chase`, `:inspect`, etc.) |
+| `src/lexer.rs`      | Breaks text into tokens like `theory`, `{`, `Sort`, `;` |
+| `src/parser.rs`     | Builds a tree structure from tokens |
+| `src/ast.rs`        | Defines what the tree structure looks like |
+| `src/core.rs`       | The "verified" internal representation |
+| `src/elaborate/`    | Type checking and name resolution |
+| `src/store/`        | Saving/loading data, version control |
+| `src/query/`        | The chase algorithm lives here |
+| `src/solver/`       | Model search (finding valid instances) |
+| `src/tensor/`       | Efficient rule checking with sparse matrices |
+| `src/cc.rs`         | Congruence closure — tracks equalities |
+| `examples/geolog/`  | 30+ example files you can learn from |
+| `tests/`            | Automated tests |
+| `docs/`             | Documentation (ARCHITECTURE.md, SYNTAX.md) |
+
+---
+
+## Key Entry Points
+
+If you're reading the code, start here:
+
+| What You Want | Where To Look |
+|---------------|---------------|
+| How the CLI starts | `src/bin/geolog.rs` |
+| How files are parsed | `src/lib.rs::parse()` |
+| How REPL commands work | `src/repl.rs::ReplState::process_line()` |
+| How theories are checked | `src/elaborate/theory.rs::elaborate_theory()` |
+| How instances are built | `src/elaborate/instance.rs::elaborate_instance_ctx()` |
+| How facts are derived | `src/query/chase.rs::chase_fixpoint_with_cc()` |
+| How models are searched | `src/solver/mod.rs::enumerate_models()` |
+
+---
+
+## REPL Commands
+
+When you run `geolog` interactively, these commands are available:
+
+```
+:list                  - Show all theories and instances
+:inspect Triangle      - Show details of "Triangle" instance
+
+:add Triangle v : V;   - Add element v to Triangle
+:assert [x:a, y:b] R;  - Assert a relation holds
+:retract [x:a, y:b] R; - Remove a relation
+
+:chase Triangle        - Derive all consequences from axioms
+:solve MyInstance      - Search for a valid model
+
+:commit "message"      - Save current state (like git commit)
+:history               - Show past commits
+
+:source file.geolog    - Load and run a file
+:help                  - Show help
+```
+
+### Example Session
+
+```
+$ cargo run -- examples/geolog/graph.geolog
+> :list
+Theories: Graph
+Instances: Triangle
+
+> :inspect Triangle
+Instance Triangle : Graph
+  Carriers:
+    V: {A, B, C}
+    E: {ab, bc, ca}
+  Functions:
+    src: {ab -> A, bc -> B, ca -> C}
+    tgt: {ab -> B, bc -> C, ca -> A}
+```

notes/002-design-decisions.md

@@ -0,0 +1,215 @@
+# Design Decisions
+
+This document explains *why* Geolog works the way it does.
+
+---
+
+## Geometric Logic: What It Means
+
+Geolog uses "geometric logic" — a restricted form of logic that can express:
+- "If X then Y" rules
+- "There exists something such that..."
+- "A or B" (but you can't say "not A")
+
+**What you CAN write:**
+```
+// If x and y are both connected to z, they know each other
+forall x, y, z. connected(x,z), connected(y,z) |- knows(x,y)
+
+// Every person has a best friend
+forall p : Person. |- exists f : Person. best_friend(p, f)
+
+// Every task is either done or pending
+forall t : Task. |- done(t) \/ pending(t)
+```
+
+**What you CANNOT write:**
+```
+// No negation allowed
+forall x. |- not blocked(x)           // INVALID
+
+// No "if not" patterns
+forall x. not done(x) |- pending(x)   // INVALID
+```
+
+**Why this restriction?** Geometric logic has nice mathematical properties — it's preserved by "geometric morphisms" between topoi. This isn't just theory; it means the reasoning is compositional and predictable.
+
+---
+
+## Postfix Function Application
+
+Most languages write `f(x)` to apply function `f` to `x`. Geolog writes `x f`.
+
+```
+// Traditional notation
+src(ab)           // "apply src to ab"
+
+// Geolog notation
+ab src            // "ab, then src"
+```
+
+**Why?** It matches how you read pipelines left-to-right:
+
+```
+// Geolog: read left to right
+ab src tgt        // "take ab, get its src, get that's tgt"
+
+// Traditional: read inside out
+tgt(src(ab))      // "tgt of src of ab"
+```
+
+This is called "categorical" style because it matches how mathematicians compose morphisms in category theory.
+
+---
+
+## Identity System: Luids and Slids
+
+Geolog needs to track elements across different operations. It uses two kinds of IDs:
+
+| ID Type | Scope | Example |
+|---------|-------|---------|
+| **Luid** (Local Universe ID) | Global — unique across everything | "Element #4827" |
+| **Slid** (Structure-Local ID) | Local — index within one structure | "The 3rd vertex" |
+
+**Why both?**
+- Slids are small integers (0, 1, 2...) — fast for computation
+- Luids persist across saves/loads — you can reference "that specific vertex" forever
+
+```
+Structure "Triangle":
+  Vertex A has Slid=0, Luid=1001
+  Vertex B has Slid=1, Luid=1002
+  Vertex C has Slid=2, Luid=1003
+
+After merging A and B (because an axiom said A = B):
+  Vertex A has Slid=0, Luid=1001 (canonical)
+  Vertex B → now points to A
+```
+
+---
+
+## Append-Only Storage
+
+Geolog never deletes data. When you "remove" something, it's marked as removed but still stored.
+
+**Why?**
+- Perfect audit trail — you can see exactly what changed and when
+- Safe undo — nothing is ever lost
+- Git-like history — you can go back to any previous state
+
+```
+Commit 1: Added vertices A, B, C
+Commit 2: Added edge ab
+Commit 3: Marked edge ab as "removed"  ← still stored, just flagged
+```
+
+---
+
+## Type System
+
+### Sorts (Types)
+
+A **sort** is a type of thing. Vertices and Edges are different sorts:
+
+```geolog
+theory Graph {
+  V : Sort;    // V is a type (the type of vertices)
+  E : Sort;    // E is a type (the type of edges)
+}
+```
+
+### Functions
+
+Functions map elements to elements:
+
+```geolog
+src : E -> V;              // Every edge has a source vertex
+tgt : E -> V;              // Every edge has a target vertex
+mul : [x: M, y: M] -> M;   // Binary function taking a pair
+```
+
+The `[x: M, y: M]` is a **product domain** — the function takes a record with two fields.
+
+### Relations
+
+Relations are yes/no questions about tuples:
+
+```geolog
+leq : [x: X, y: X] -> Prop;   // "Is x ≤ y?"
+connected : [a: V, b: V] -> Prop;
+```
+
+`Prop` means "proposition" — it's either true or false for each input.
+
+---
+
+## Chase Algorithm Design
+
+The chase repeatedly applies rules until nothing new can be derived:
+
+```
+Initial facts: friends(alice, bob), friends(bob, charlie)
+Rule: friends(x,y), friends(y,z) |- knows(x,z)
+
+Iteration 1:
+  - Rule matches with x=alice, y=bob, z=charlie
+  - Conclusion knows(alice, charlie) is missing
+  - Add: knows(alice, charlie)
+
+Iteration 2:
+  - No rule has missing conclusions
+  - Stop (fixpoint reached)
+
+Final facts: friends(alice, bob), friends(bob, charlie), knows(alice, charlie)
+```
+
+**Key features:**
+- Uses **tensor algebra** to efficiently find which rules need to fire
+- Integrates **congruence closure** so `x = y` conclusions actually merge elements
+- **Terminates** for theories with identity elements (earlier versions could loop forever)
+
+---
+
+## Solver Architecture
+
+When you need to *find* a model (not just derive facts), the solver searches:
+
+```
+Goal: Find an instance of Graph with a cycle
+
+Search tree:
+  Node 1: Empty graph
+    → Obligation: need at least one edge (from some axiom)
+    → Branch: try adding edge e1
+
+  Node 2: Graph with e1
+    → Obligation: e1 needs src and tgt
+    → Branch: try src(e1) = v1, tgt(e1) = v1 (self-loop!)
+
+  Node 3: Graph with e1, v1, self-loop
+    → All axioms satisfied
+    → SUCCESS: return this model
+```
+
+**Key features:**
+- **Explicit search tree** — the solver builds a tree structure, not recursive function calls
+- **Tactics** — different strategies (forward chaining, equation propagation) can be combined
+- **Obligations** — "this axiom requires a witness" is tracked explicitly
+
+---
+
+## Query Compilation
+
+Queries are compiled to relational algebra (like SQL internally):
+
+```
+Query: Find all x,y where connected(x,y) and connected(y,x)
+
+Compiled plan:
+  1. Scan relation "connected" → get all (x,y) pairs
+  2. Scan relation "connected" → get all (a,b) pairs
+  3. Join where y=a and x=b
+  4. Project out x,y
+```
+
+This is optimized with standard database techniques (filter pushdown, etc.).

notes/003-project-status.md

@@ -0,0 +1,152 @@
+# Project Status
+
+**Version:** 0.1.0 (Early stage, but functional)
+
+---
+
+## Codebase Size
+
+| What | Count |
+|------|-------|
+| Rust source code | ~30,000 lines |
+| Test code | ~8,000 lines |
+| Example `.geolog` files | ~2,300 lines across 30 files |
+| Source files | 84 |
+| Unit tests | 137 (all passing) |
+| Integration tests | 31 (all passing) |
+
+---
+
+## What Works Well
+
+These features are complete and reliable:
+
+### Core Engine
+- **Parser** — reads `.geolog` files, gives helpful error messages
+- **Type checker** — catches mistakes like using undefined sorts
+- **Chase algorithm** — derives facts from rules correctly
+- **Equality handling** — when rules say `x = y`, elements are properly merged
+
+### Examples That Run
+```bash
+cargo run -- examples/geolog/graph.geolog        # Simple directed graph
+cargo run -- examples/geolog/preorder.geolog     # Reflexive, transitive relation
+cargo run -- examples/geolog/transitive_closure.geolog  # Shows chase in action
+cargo run -- examples/geolog/category.geolog     # Category theory basics
+```
+
+### Interactive Features
+- REPL with command history
+- Inspect any theory or instance
+- Run chase interactively
+- Save/load with version history
+
+---
+
+## What Mostly Works
+
+These features work but have limitations:
+
+### Parameterized Theories
+You can define theories that depend on other instances:
+
+```geolog
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;  // References N's places
+}
+```
+
+**Limitation:** Nested instances (instances inside instances) only partially work.
+
+### Model Search
+The solver can find models satisfying axioms, but:
+- Works best for small models
+- Some search strategies are incomplete
+- No timeout handling
+
+---
+
+## Known Gaps
+
+### Things That Don't Work Yet
+
+| Feature | Status |
+|---------|--------|
+| Product types in conclusions | Functions returning records don't fully work |
+| Existentials over products | `exists p : [x:M, y:M]. ...` fails |
+| Field projections in equations | `x.field = y` doesn't compile |
+
+### Example of What Fails
+
+```geolog
+// This works:
+forall x : M. |- exists y : M. f(x) = y
+
+// This doesn't work (product sort in existential):
+forall x : M. |- exists p : [a:M, b:M]. g(x) = p
+```
+
+### Silent Failures
+
+When the tensor compiler can't handle an axiom, it **silently skips it**. This can be confusing — your axiom looks fine but nothing happens.
+
+```geolog
+// This axiom might be silently skipped if it has unsupported patterns:
+ax/complex : forall x. premise |- [a: x, b: x] some_relation;
+// No error, but also no effect
+```
+
+---
+
+## TODOs in the Code
+
+These are marked in the source with `// TODO`:
+
+| Location | What's Missing |
+|----------|----------------|
+| `src/repl.rs:84` | Theory type not fully stored in metadata |
+| `src/overlay.rs:380` | Copying functions between structures |
+| `src/store/query.rs:61` | Batch loading for better performance |
+| `src/store/instance.rs` | External references between instances |
+| `src/query/to_relalg.rs` | Some relational operators |
+
+---
+
+## Test Coverage
+
+### What's Tested
+
+| Area | Tests |
+|------|-------|
+| Type checking | 14 unit tests |
+| Chase algorithm | Comprehensive unit tests |
+| Parser | 4 unit tests + snapshot tests |
+| Examples | 31 integration tests (one per example file) |
+| Random inputs | 11 property-based test suites |
+
+### Running Tests
+
+```bash
+cargo test              # Run all tests
+cargo test unit_chase   # Run only chase tests
+cargo test --release    # Run with optimizations (faster)
+```
+
+### Fuzzing
+
+The `fuzz/` directory has fuzzing targets that generate random inputs to find crashes:
+
+```bash
+cargo +nightly fuzz run fuzz_parser
+```
+
+---
+
+## What's Being Worked On
+
+According to code comments and structure:
+
+1. **Lean4 formalization** — Mathematical proofs about correctness (in `proofs/`)
+2. **Better disjunction handling** — Currently fires both branches, should choose one
+3. **Query plan improvements** — More efficient execution

notes/004-key-concepts.md

@@ -0,0 +1,273 @@
+# Key Concepts
+
+This document explains the main ideas in Geolog without assuming math background.
+
+---
+
+## Theories and Instances
+
+A **theory** is a template — it defines what *kinds* of things exist and what rules they follow.
+
+An **instance** is a concrete example — actual things that follow the theory's rules.
+
+### Example: Graphs
+
+```geolog
+// The theory: "A graph has vertices and edges"
+theory Graph {
+  V : Sort;           // There's a kind of thing called "vertex"
+  E : Sort;           // There's a kind of thing called "edge"
+  src : E -> V;       // Every edge has a source vertex
+  tgt : E -> V;       // Every edge has a target vertex
+}
+
+// An instance: A specific triangle graph
+instance Triangle : Graph = {
+  // Three vertices
+  A : V;
+  B : V;
+  C : V;
+
+  // Three edges forming a triangle
+  ab : E;
+  ab src = A;    // Edge ab goes from A...
+  ab tgt = B;    // ...to B
+
+  bc : E;
+  bc src = B;
+  bc tgt = C;
+
+  ca : E;
+  ca src = C;
+  ca tgt = A;
+}
+```
+
+Think of it like:
+- **Theory** = "A spreadsheet template with certain columns"
+- **Instance** = "A filled-in spreadsheet"
+
+---
+
+## Axioms (Rules)
+
+An **axiom** tells Geolog: "Whenever the left side is true, make the right side true too."
+
+```
+forall x, y, z. friends(x,y), friends(y,z) |- knows(x,z)
+        ↑              ↑                         ↑
+   "for any x,y,z"  "if these are true"    "then this must be true"
+```
+
+### Simple Example: Transitivity
+
+"If A ≤ B and B ≤ C, then A ≤ C"
+
+```geolog
+theory Preorder {
+  X : Sort;
+  leq : [x: X, y: X] -> Prop;  // "x ≤ y" relation
+
+  // Transitivity rule
+  ax/trans : forall x: X, y: X, z: X.
+    [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
+}
+```
+
+### What `[x: x, y: y] leq` Means
+
+This is Geolog's way of writing `leq(x, y)` or "x ≤ y":
+
+```
+[x: x, y: y] leq
+    ↑           ↑
+ a record     applied to the "leq" relation
+ with fields
+ x and y
+```
+
+It's like calling a function with named parameters: `leq(x=x, y=y)`.
+
+---
+
+## The Chase Algorithm
+
+The **chase** is what makes Geolog useful. It automatically applies your rules to derive new facts.
+
+### Step-by-Step Example
+
+**Setup:**
+```geolog
+theory Friends {
+  Person : Sort;
+  friends : [a: Person, b: Person] -> Prop;
+  knows : [a: Person, b: Person] -> Prop;
+
+  // Rule: friends-of-friends know each other
+  ax/fof : forall x, y, z : Person.
+    [a: x, b: y] friends, [a: y, b: z] friends |- [a: x, b: z] knows;
+}
+
+instance Group : Friends = {
+  alice : Person;
+  bob : Person;
+  charlie : Person;
+
+  [a: alice, b: bob] friends;      // Alice and Bob are friends
+  [a: bob, b: charlie] friends;    // Bob and Charlie are friends
+}
+```
+
+**Running the chase:**
+
+```
+Initial state:
+  friends = {(alice, bob), (bob, charlie)}
+  knows = {}
+
+Chase iteration 1:
+  Looking at axiom ax/fof...
+  Found match: x=alice, y=bob, z=charlie
+    - [a:alice, b:bob] friends? YES
+    - [a:bob, b:charlie] friends? YES
+    - [a:alice, b:charlie] knows? NO ← violation!
+  Fire conclusion: add [a:alice, b:charlie] knows
+
+  knows = {(alice, charlie)}  ← NEW FACT
+
+Chase iteration 2:
+  Looking at axiom ax/fof...
+  No new violations found.
+  DONE (fixpoint reached)
+
+Final state:
+  friends = {(alice, bob), (bob, charlie)}
+  knows = {(alice, charlie)}
+```
+
+### The Key Insight
+
+You don't write a program to derive facts. You write *rules*, and Geolog figures out everything that follows from them.
+
+---
+
+## Union-Find (Equality Tracking)
+
+When a rule concludes that two things are equal (`x = y`), Geolog needs to merge them. It uses a data structure called **union-find**.
+
+### The Problem
+
+```geolog
+// Rule: If two people have the same ID, they're the same person
+ax/same_id : forall p, q : Person, i : ID.
+  [p: p] id = i, [p: q] id = i |- p = q;
+```
+
+If this rule fires with `p = alice` and `q = alicia`, Geolog learns that `alice = alicia`. But now every reference to `alicia` should really mean `alice`.
+
+### How Union-Find Works
+
+```
+Before:
+  alice → alice (points to itself)
+  alicia → alicia (points to itself)
+
+After union(alice, alicia):
+  alice → alice (the "representative")
+  alicia → alice (now points to alice)
+
+Later, find(alicia) returns alice
+```
+
+**Why not just use a dictionary?**
+
+| Approach | Cost of merging N elements |
+|----------|---------------------------|
+| Dictionary + Sets | O(N) — must update every element |
+| Union-Find | O(1) — just change one pointer |
+
+When rules derive thousands of equalities, this matters.
+
+---
+
+## Existentials (Creating New Things)
+
+Rules can say "there must exist something":
+
+```geolog
+// Every person has a best friend
+ax/has_bf : forall p : Person. |- exists f : Person. [p: p, f: f] best_friend;
+```
+
+When the chase processes this:
+
+1. **Check:** Does person `p` already have a best friend?
+2. **If yes:** Do nothing
+3. **If no:** Create a new person and make them `p`'s best friend
+
+```
+Before chase:
+  Persons = {alice, bob}
+  best_friend = {}
+
+After chase:
+  Persons = {alice, bob, fresh_1, fresh_2}
+  best_friend = {(alice, fresh_1), (bob, fresh_2)}
+```
+
+The chase created `fresh_1` and `fresh_2` because the axiom demanded witnesses.
+
+---
+
+## Disjunctions (Or)
+
+Rules can have "or" in conclusions:
+
+```geolog
+// Every task is either done or pending
+ax/status : forall t : Task. |- [t: t] done \/ [t: t] pending;
+```
+
+**Current behavior:** Geolog fires *both* branches. So every task becomes both done AND pending.
+
+**Why?** Proper disjunction handling requires backtracking search, which is complex. The current approach is "sound" (never wrong) but "incomplete" (may add more facts than necessary).
+
+---
+
+## Tensor Algebra (How Chase Is Fast)
+
+Checking "which rules have violations" naively requires checking every possible variable assignment. For 100 people and 3 variables, that's 100³ = 1,000,000 checks.
+
+Geolog uses **sparse tensors** (think: sparse matrices, but multi-dimensional) to do this efficiently:
+
+```
+Relations are stored as sparse tensors:
+  friends[i][j] = 1 if person i and person j are friends
+
+Finding violations becomes tensor operations:
+  violations = friends ⊗ friends ⊗ (1 - knows)
+                  ↑          ↑           ↑
+              "x,y friends" "y,z friends" "x,z not known"
+```
+
+This is much faster than nested loops because:
+- Sparse storage skips empty cells
+- Tensor operations are highly optimized
+- Results are computed in bulk, not one-by-one
+
+---
+
+## What Geolog Can't Express
+
+Geometric logic intentionally excludes some things:
+
+| Can't Write | Why Not |
+|-------------|---------|
+| `not R(x)` | No negation — can't say "x is NOT red" |
+| `if not A then B` | No negation in premises |
+| `x + 1 = y` | No arithmetic — this isn't a calculator |
+| `forall x. R(x)` with no conclusion | Axioms must have conclusions |
+
+**This is by design.** These restrictions make the logic "geometric," which has nice theoretical properties (preserved by geometric morphisms, has models in any topos, etc.).
+
+For practical purposes: Geolog is good for "if-then" rules and "there exists" statements, not for arithmetic or negation.

notes/005-critical-assessment.md

@@ -0,0 +1,179 @@
+# Critical Assessment
+
+This document takes a skeptical look at what Geolog actually is versus what the documentation suggests.
+
+---
+
+## Origin
+
+Geolog was generated by an AI (Claude Opus 4.5). From the README:
+
+> "This README was synthesized automatically by Claude Opus 4.5. As was this entire project, really."
+
+This is unusual — most software is written by humans over time. Geolog was generated in a relatively short period, which has implications:
+
+**Positives:**
+- Consistent code style throughout
+- Good test coverage from the start
+- Clean architecture
+
+**Concerns:**
+- No organic evolution based on real user feedback
+- No battle-testing in production environments
+- Design decisions may be theoretically elegant but practically awkward
+
+---
+
+## Claimed vs. Actual Use Cases
+
+### Claim: "Business Process Workflow Orchestration"
+
+**What this suggests:** You could use Geolog to manage business workflows — approve orders, route documents, handle exceptions.
+
+**Reality:** Geolog is a command-line REPL. It has:
+- No REST API
+- No integration with external systems
+- No notification system
+- No user interface
+- No distributed execution
+- No failure recovery
+
+**What real workflow tools have:** Temporal, Camunda, and Airflow handle retries, timeouts, external service calls, monitoring dashboards, and run across multiple servers.
+
+**Verdict:** Geolog can *model* a workflow on paper. It cannot *run* a workflow in production.
+
+---
+
+### Claim: "Formal Verification"
+
+**What this suggests:** You could use Geolog to prove your software is correct.
+
+**Reality:**
+- The Lean4 proofs in `proofs/` are "in progress"
+- There's no connection between Geolog models and actual code
+- No proof certificates are generated
+
+**What real verification tools have:** Coq, Lean, and TLA+ have decades of development, extensive libraries, extraction to executable code, and industrial use (CompCert, seL4, Amazon's use of TLA+).
+
+**Verdict:** Geolog has some formal foundations but is not a verification tool.
+
+---
+
+### Claim: "Database Query Design"
+
+**What this suggests:** You could use Geolog for database work.
+
+**Reality:**
+- Data lives in memory (with optional file persistence)
+- No SQL interface
+- No transactions
+- No concurrent access
+- No indexing for large datasets
+- No connection to actual databases
+
+**What real database tools have:** PostgreSQL, SQLite, and even embedded databases handle concurrent writes, ACID transactions, and gigabytes of data.
+
+**Verdict:** Geolog has relational algebra internally for a different purpose. It's not a database.
+
+---
+
+### Claim: "Petri Net Reachability"
+
+**What this suggests:** You could analyze Petri nets with Geolog.
+
+**Reality:** This is the most honest claim. The examples show Petri net modeling:
+
+```geolog
+theory PetriNet {
+  P : Sort;  // Places
+  T : Sort;  // Transitions
+  pre : [t: T, p: P] -> Prop;   // Input arcs
+  post : [t: T, p: P] -> Prop;  // Output arcs
+}
+```
+
+**But:** The examples have 3-4 places. Industrial Petri net tools handle thousands of places with specialized algorithms (state space reduction, symbolic model checking).
+
+**Verdict:** Geolog can model small Petri nets. It's educational, not industrial.
+
+---
+
+## What Geolog Actually Is
+
+### Good For
+
+| Use | Why |
+|-----|-----|
+| **Learning geometric logic** | Clean implementation with good examples |
+| **Understanding chase algorithms** | The code is readable and well-commented |
+| **Experimenting with rule systems** | Quick to try ideas in the REPL |
+| **Teaching category theory concepts** | Postfix notation matches categorical thinking |
+| **Prototyping constraint systems** | Faster than writing from scratch |
+
+### Not Good For
+
+| Use | Why Not |
+|-----|---------|
+| **Production systems** | No APIs, no monitoring, no error handling |
+| **Large datasets** | Everything in memory, no optimization for scale |
+| **Real workflows** | No external integrations |
+| **Serious verification** | Incomplete proofs, no connection to real code |
+| **Anything user-facing** | It's a developer REPL, not an application |
+
+---
+
+## Technical Influences
+
+Geolog combines ideas from several fields, which is interesting but also means it's not the best tool for any single field:
+
+| Concept | From | Better Specialized Tool |
+|---------|------|------------------------|
+| Geometric logic | Mathematical logic | Lean, Coq (for proofs) |
+| Chase algorithm | Database theory | Datalog engines (for scale) |
+| Equality saturation | Program optimization | egg/egglog (more mature) |
+| Tensor operations | Linear algebra | NumPy, sparse matrix libraries |
+| Model search | SMT solving | Z3, CVC5 (much more powerful) |
+
+---
+
+## Code Quality Assessment
+
+Despite the skepticism above, the code itself is well-done:
+
+**Positives:**
+- Comprehensive tests (168 passing)
+- Good error messages with source locations
+- Clean module separation
+- Documented design decisions
+
+**Negatives:**
+- Some silent failures (tensor compilation)
+- Incomplete features (product types)
+- No performance benchmarks
+- Limited real-world testing
+
+---
+
+## Who Should Use This?
+
+**Yes:**
+- Students learning about logic and type systems
+- Researchers exploring geometric logic
+- Developers curious about chase algorithms
+- Anyone wanting to understand equality saturation
+
+**No:**
+- Teams building production systems
+- Anyone needing a database
+- Anyone needing workflow automation
+- Anyone needing formal guarantees
+
+---
+
+## Bottom Line
+
+Geolog is a **well-crafted educational project**, not production infrastructure.
+
+The code is clean, tests pass, and the examples work. But the claimed "use cases" are aspirational — describing what geometric logic *could theoretically* be used for, not what this specific tool is ready to do.
+
+If you want to learn about geometric logic and chase algorithms, Geolog is excellent. If you want to solve real problems, use established tools in each domain.

notes/006-missing-components.md

@@ -0,0 +1,342 @@
+# Missing Components
+
+*Assuming Geolog's core is mature and stable, what would be needed to make it production-ready?*
+
+---
+
+## Summary
+
+Geolog has a solid **core engine** (parser, type checker, chase, tensor algebra) but is missing everything around it:
+
+- **No way in** — no API, no language bindings
+- **No way to scale** — no parallelism, no indexes, no query optimization
+- **No way to operate** — no concurrency, no recovery, no monitoring
+- **No way to debug** — no logging, no traces, no profiling
+
+It's a well-built engine without a car around it.
+
+---
+
+## 1. Integration & APIs
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **REST API** | Can't call Geolog from web apps, microservices, or other languages |
+| **Language bindings** | No Python, JavaScript, or FFI — Rust-only |
+| **LSP (Language Server)** | No IDE autocomplete, error squiggles, go-to-definition |
+| **JSON/YAML serialization** | Only binary format (rkyv) — can't inspect data externally |
+| **Async API** | All operations block — can't integrate with async runtimes |
+
+### What Integration Would Look Like
+
+```python
+# This doesn't exist today
+from geolog import Theory, Instance
+
+theory = Theory.parse("""
+    theory Graph {
+        V : Sort;
+        E : Sort;
+        src : E -> V;
+        tgt : E -> V;
+    }
+""")
+
+instance = Instance.create(theory)
+instance.add_element("V", "alice")
+instance.add_element("V", "bob")
+instance.add_element("E", "edge1")
+instance.set_function("edge1", "src", "alice")
+instance.set_function("edge1", "tgt", "bob")
+
+# Run chase and get results as JSON
+results = instance.chase()
+print(results.to_json())
+```
+
+```bash
+# REST API that doesn't exist
+curl -X POST http://localhost:8080/chase \
+  -H "Content-Type: application/json" \
+  -d '{"instance": "MyGraph", "max_iterations": 100}'
+```
+
+---
+
+## 2. Performance & Scale
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **Cost-based query optimizer** | No cardinality estimates — can't choose optimal join order |
+| **Secondary indexes** | Only RoaringBitmaps — no B-trees for range queries |
+| **Parallel execution** | Single-threaded only |
+| **Benchmark suite** | No way to track performance regressions |
+| **Memory profiling** | No visibility into allocation patterns |
+
+### What Would Struggle
+
+```
+Scenario: Theory with 10,000 elements and 50 axioms
+
+Problems:
+→ No way to predict which axioms are expensive
+→ No parallel chase execution
+→ No index to speed up specific lookups
+→ No benchmark to know if changes made it slower
+```
+
+### What's Needed
+
+```rust
+// Cost-based optimizer (doesn't exist)
+let plan = optimizer.compile(query);
+println!("Estimated cost: {}", plan.estimated_cost());
+println!("Join order: {:?}", plan.join_order());
+
+// Parallel chase (doesn't exist)
+let results = chase_parallel(axioms, structure, num_threads=4);
+
+// Benchmarks (don't exist)
+// benches/chase_benchmark.rs
+// benches/tensor_benchmark.rs
+```
+
+---
+
+## 3. Solver Intelligence
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **Search heuristics** | Breadth-first only — no intelligent variable/value ordering |
+| **Backtracking** | Can't explore branches — only refines single partial model |
+| **Lemma learning** | No conflict-driven learning (CDCL) like modern SAT/SMT solvers |
+| **External prover integration** | Can't delegate to Z3, Lean, or Coq |
+
+### Current Behavior
+
+```
+Solver tries everything in order:
+  x = 1? Try it.
+  x = 2? Try it.
+  x = 3? Try it.
+  ...
+
+No learning from failures.
+No "this variable is most constrained, try it first."
+```
+
+### What Modern Solvers Do
+
+```
+CDCL (Conflict-Driven Clause Learning):
+  1. Try x = 1
+  2. Conflict detected!
+  3. Learn: "x ≠ 1" (add as constraint)
+  4. Backtrack and never try x = 1 again
+
+Variable ordering:
+  1. Count constraints on each variable
+  2. Try most-constrained variable first
+  3. Fail fast, prune search space early
+```
+
+---
+
+## 4. Reliability & Operations
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **Multi-user concurrency** | No locking — can't have multiple writers |
+| **ACID transactions** | No rollback on failure |
+| **Write-ahead log (WAL)** | No crash recovery |
+| **Replication** | No distributed deployment |
+| **Garbage collection** | Tombstoned elements accumulate forever |
+| **Compression** | Data size grows unbounded |
+
+### Production Scenario That Fails
+
+```
+User A: :chase BigInstance     (starts running)
+User B: :add BigInstance x:V;  (modifies while A is running)
+
+Result: Race condition, possible data corruption
+No way to recover if either crashes mid-operation
+No way to rollback User B's change if it breaks something
+```
+
+### What's Needed
+
+```rust
+// Transactions (don't exist)
+let tx = store.begin_transaction();
+tx.add_element("V", "new_vertex")?;
+tx.chase("MyInstance")?;
+tx.commit()?;  // Or tx.rollback() on error
+
+// Concurrency control (doesn't exist)
+let lock = store.write_lock("MyInstance");
+// ... safe modifications ...
+drop(lock);
+
+// Crash recovery (doesn't exist)
+// WAL ensures operations are durable before acknowledging
+```
+
+---
+
+## 5. Developer Experience
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **Logging framework** | No structured logs for debugging |
+| **Interactive debugger** | Can't step through solver decisions |
+| **Execution traces** | Can't replay what happened |
+| **IDE plugin** | No syntax highlighting, no error squiggles |
+| **Tutorials** | Only reference docs, no guided learning |
+
+### Debugging Today
+
+```
+> :chase MyInstance
+// Something went wrong... but what?
+// No logs, no trace, just the final state
+// Which axiom fired? Which elements were created? Unknown.
+```
+
+### What's Needed
+
+```
+// Structured logging (doesn't exist)
+[2026-03-19 10:30:01] INFO  chase: Starting chase on MyInstance
+[2026-03-19 10:30:01] DEBUG chase: Axiom ax/trans fired with {x: v1, y: v2, z: v3}
+[2026-03-19 10:30:01] DEBUG chase: Added relation [x:v1, y:v3] leq
+[2026-03-19 10:30:02] INFO  chase: Fixpoint reached after 3 iterations
+
+// Interactive debugger (doesn't exist)
+> :debug chase MyInstance
+Breakpoint at axiom ax/trans
+  Variables: x=v1, y=v2, z=v3
+  Action: Add [x:v1, y:v3] leq
+(debug) step
+(debug) inspect structure
+(debug) continue
+```
+
+---
+
+## 6. Error Handling
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **Typed error enums** | All errors are strings — can't handle programmatically |
+| **Error recovery suggestions** | "Did you mean X?" doesn't exist |
+| **Partial results** | If 90% succeeds, you get nothing |
+| **Stack traces** | Limited context for where errors occur |
+
+### Current State
+
+```rust
+// All errors are just strings
+fn elaborate_theory(...) -> Result<Theory, String>
+
+// Can only display, not handle programmatically
+match result {
+    Err(msg) => println!("{}", msg),  // That's all you can do
+}
+```
+
+### What's Needed
+
+```rust
+enum GeologError {
+    Parse(ParseError),
+    Type(TypeError),
+    Chase(ChaseError),
+    Solver(SolverError),
+}
+
+enum ParseError {
+    UnexpectedToken { span: Span, found: Token, expected: Vec<Token> },
+    UnterminatedString { span: Span },
+    // ...
+}
+
+enum TypeError {
+    UndefinedSort { name: String, span: Span, similar: Vec<String> },
+    TypeMismatch { expected: Type, found: Type, span: Span },
+    // ...
+}
+
+// Now you can handle errors programmatically
+match result {
+    Err(GeologError::Type(TypeError::UndefinedSort { name, similar, .. })) => {
+        println!("Unknown sort '{}'. Did you mean '{}'?", name, similar[0]);
+    }
+    // ...
+}
+```
+
+---
+
+## 7. Missing Language Features
+
+| Missing | Why It Matters |
+|---------|----------------|
+| **Modules/imports** | Can't organize large theories into files |
+| **Parameterized axioms** | Can't write generic rules that work across sorts |
+| **Arithmetic** | No `x + 1 = y` or `count > 0` |
+| **Aggregation** | No `count`, `sum`, `max` over relations |
+| **Stratified negation** | No "if NOT X" even in limited safe form |
+
+### What You Can't Express
+
+```geolog
+// Modules (don't exist)
+import std/graph;
+import std/preorder;
+
+// Arithmetic (doesn't exist)
+ax/increment : forall x : Nat. |- successor(x) = x + 1;
+
+// Aggregation (doesn't exist)
+ax/has_friends : forall p : Person.
+    count([f: f] friend_of(p, f)) > 0 |- popular(p);
+
+// Stratified negation (doesn't exist)
+ax/lonely : forall p : Person.
+    not exists f : Person. friend_of(p, f) |- lonely(p);
+```
+
+---
+
+## Priority Ranking
+
+If making Geolog production-ready:
+
+| Priority | Component | Effort | Impact |
+|----------|-----------|--------|--------|
+| 1 | REST API | Medium | Unlocks all integrations |
+| 2 | LSP server | Medium | Makes language usable in IDEs |
+| 3 | Structured errors | Low | Enables better tooling |
+| 4 | Benchmark suite | Low | Enables performance work |
+| 5 | Logging/tracing | Low | Enables debugging |
+| 6 | Concurrency/locking | High | Required for multi-user |
+| 7 | Solver heuristics | High | Makes solver practical |
+| 8 | Cost-based optimizer | High | Enables scale |
+| 9 | Language bindings | Medium | Broader adoption |
+| 10 | Modules/imports | Medium | Enables large projects |
+
+---
+
+## Maturity by Area
+
+| Area | Maturity | What Exists | Critical Gap |
+|------|----------|-------------|--------------|
+| **Query** | 70% | Chase, optimization, temporal ops | No cost-based optimization |
+| **Solver** | 65% | Explicit tree, tactics framework | No heuristics, no backtracking |
+| **Storage** | 75% | Append-only, versioning | No concurrency, no recovery |
+| **API** | 45% | Clean Rust library | No REST, no LSP, no FFI |
+| **Performance** | 40% | Fuzzing, property tests | No benchmarks, no profiling |
+| **Debugging** | 50% | Error formatting, query plans | No logging, no debugger |
+| **Errors** | 60% | Recoverable, source spans | String-only, limited context |
+| **Docs** | 65% | Architecture, inline comments | No IDE support, no tutorials |

notes/NOTES.md

@@ -1,322 +0,0 @@
-# Geolog Project Notes
-
-## Overview
-
-**Geolog** is a **Geometric Logic REPL** — a type theory with semantics in topoi, designed for formal specifications
-using geometric logic.
-
-### Core Capabilities
-
-- **Geometric logic programming** — encode mathematical structures, relationships, and constraints
-- **Database schema definition** — define sorts, functions, relations, and axioms
-- **Model/instance creation** — create concrete finite models satisfying theory axioms
-- **Automated inference** — chase algorithm for automatic fact derivation
-- **Version control** — git-like commits and tracking for instances
-- **Persistence** — append-only storage with optional disk persistence
-
-### Use Cases
-
-- Business process workflow orchestration
-- Formal verification via diagrammatic rewriting
-- Database query design
-- Petri net reachability and process modeling
-
----
-
-## Tech Stack
-
-**Primary Language**: Rust (2021 edition, Cargo-based)
-
-### Key Dependencies
-
-| Crate               | Version | Purpose                             |
-|---------------------|---------|-------------------------------------|
-| `chumsky`           | 0.9     | Parser combinator library           |
-| `ariadne`           | 0.4     | Error reporting with source spans   |
-| `rkyv`              | 0.7     | Zero-copy serialization             |
-| `rustyline`         | 15      | REPL readline interface             |
-| `egglog-union-find` | 1.0     | Union-find for congruence closure   |
-| `roaring`           | 0.10    | Bitmap library for sparse relations |
-| `indexmap`          | 2.0     | Order-preserving hash maps          |
-| `uuid`              | 1       | UUID generation                     |
-| `memmap2`           | 0.9     | Memory-mapped file I/O              |
-
-### Testing Frameworks
-
-- `insta` — snapshot testing
-- `proptest` — property-based testing
-- `tempfile` — temporary directory management
-
----
-
-## Architecture
-
-```
-┌─────────────────────────────────────────────────────┐
-│                    USER INTERFACE                    │
-│  REPL (interactive CLI) | Batch file loading         │
-├─────────────────────────────────────────────────────┤
-│         PARSING LAYER (Lexer → Parser → AST)         │
-│  chumsky-based lexer & parser, source error reporting│
-├─────────────────────────────────────────────────────┤
-│           ELABORATION LAYER (AST → Core IR)          │
-│  Type checking, name resolution, theory/instance     │
-├─────────────────────────────────────────────────────┤
-│            CORE LAYER (Typed Representation)         │
-│  Signature, Term, Formula, Structure, ElaboratedTheory│
-├─────────────────────────────────────────────────────┤
-│              STORAGE LAYER (Persistence)             │
-│  Append-only GeologMeta store with version control   │
-├─────────────────────────────────────────────────────┤
-│            QUERY & SOLVER LAYER (Execution)          │
-│  Chase algorithm, congruence closure, relational     │
-│  algebra compiler, SMT-style model enumeration       │
-├─────────────────────────────────────────────────────┤
-│         TENSOR ALGEBRA (Axiom Checking)              │
-│  Sparse tensor evaluation for axiom validation       │
-└─────────────────────────────────────────────────────┘
-```
-
----
-
-## Directory Structure
-
-| Path                | Purpose                                      |
-|---------------------|----------------------------------------------|
-| `src/bin/geolog.rs` | CLI entry point                              |
-| `src/lib.rs`        | Library root, exports `parse()`              |
-| `src/repl.rs`       | Interactive REPL state machine               |
-| `src/lexer.rs`      | Tokenization using chumsky                   |
-| `src/parser.rs`     | Token stream → AST                           |
-| `src/ast.rs`        | Abstract syntax tree types                   |
-| `src/core.rs`       | Core IR: Signature, Term, Formula, Structure |
-| `src/elaborate/`    | AST → Core elaboration                       |
-| `src/store/`        | Persistence layer (append-only)              |
-| `src/query/`        | Chase algorithm, relational algebra          |
-| `src/solver/`       | SMT-style model enumeration                  |
-| `src/tensor/`       | Sparse tensor algebra for axiom checking     |
-| `src/cc.rs`         | Congruence closure (union-find)              |
-| `src/id.rs`         | Luid/Slid identity system                    |
-| `src/universe.rs`   | Global element registry                      |
-| `examples/geolog/`  | 30+ example `.geolog` files                  |
-| `tests/`            | 25+ test files                               |
-| `docs/`             | ARCHITECTURE.md, SYNTAX.md                   |
-| `proofs/`           | Lean4 formalization                          |
-| `fuzz/`             | Fuzzing targets                              |
-
----
-
-## Main Components
-
-### Parsing & Syntax (~1,200 lines)
-
-- `lexer.rs` — tokenization
-- `parser.rs` — token stream → AST
-- `ast.rs` — AST types (Theory, Instance, Axiom, etc.)
-- `error.rs` — error formatting with source spans
-- `pretty.rs` — Core → Geolog source roundtrip printing
-
-### Elaboration (~2,200 lines)
-
-- `elaborate/mod.rs` — coordination
-- `elaborate/theory.rs` — AST Theory → Core ElaboratedTheory
-- `elaborate/instance.rs` — AST Instance → Core Structure
-- `elaborate/env.rs` — environment with theory registry
-- `elaborate/types.rs` — type expression evaluation
-- `elaborate/error.rs` — type error reporting
-
-### Core Representation
-
-- `core.rs` — DerivedSort, Signature, Structure, Formula, Term, Sequent
-- `id.rs` — Luid (global unique ID) and Slid (structure-local ID)
-- `universe.rs` — global element registry with UUID ↔ Luid mapping
-- `naming.rs` — bidirectional name ↔ Luid mapping
-
-### Storage Layer (~1,500 lines)
-
-- `store/mod.rs` — main Store struct
-- `store/schema.rs` — cached sort/function/relation IDs
-- `store/append.rs` — low-level element append operations
-- `store/theory.rs` — theory CRUD
-- `store/instance.rs` — instance CRUD
-- `store/commit.rs` — git-like version control
-- `store/materialize.rs` — indexed views for fast lookups
-
-### Query & Compilation (~3,500 lines)
-
-- `query/compile.rs` — Query → RelAlgIR plan compilation
-- `query/to_relalg.rs` — Query → Relational Algebra IR
-- `query/from_relalg.rs` — RelAlgIR → Executable QueryOp
-- `query/chase.rs` — chase algorithm for fixpoint computation
-- `query/backend.rs` — naive QueryOp executor
-- `query/optimize.rs` — algebraic law rewriting
-
-### Solver & Model Enumeration (~1,300 lines)
-
-- `solver/mod.rs` — unified model enumeration API
-- `solver/tree.rs` — explicit search tree for partial models
-- `solver/tactics.rs` — automated search strategies:
-    - CheckTactic: axiom validation
-    - ForwardChainingTactic: Datalog-style inference
-    - PropagateEquationsTactic: congruence closure
-    - AutoTactic: composite fixpoint solver
-- `solver/types.rs` — SearchNode, Obligation, NodeStatus types
-
-### Tensor Algebra (~2,600 lines)
-
-- `tensor/expr.rs` — lazy tensor expression trees
-- `tensor/sparse.rs` — sparse tensor storage (RoaringBitmap-based)
-- `tensor/builder.rs` — expression builders
-- `tensor/compile.rs` — Formula → TensorExpr compilation
-- `tensor/check.rs` — axiom checking via tensor evaluation
-
----
-
-## Key Entry Points
-
-1. **CLI**: `src/bin/geolog.rs`
-   ```
-   Usage: geolog [-d <workspace>] [source_files...]
-   ```
-
-2. **Parse Entry**: `src/lib.rs` exports `parse(input: &str) → Result<File, String>`
-
-3. **REPL State**: `src/repl.rs` — `ReplState::process_line()`
-
-4. **Theory Elaboration**: `elaborate/theory.rs::elaborate_theory()`
-
-5. **Instance Elaboration**: `elaborate/instance.rs::elaborate_instance_ctx()`
-
-6. **Chase Algorithm**: `query/chase.rs::chase_fixpoint_with_cc()`
-
-7. **Model Enumeration**: `solver/mod.rs::enumerate_models()`
-
----
-
-## Design Decisions
-
-### Geometric Logic Foundation
-
-- **Axioms as Sequents**: `forall vars. premises |- conclusion`
-- **Positive Conclusions**: Can have existentials, disjunctions, but never negations
-- **Geometric Morphisms**: Preserved by design, enabling category-theoretic semantics
-
-### Identity System
-
-- **Luid** ("Local Universe ID"): Globally unique across all structures
-- **Slid** ("Structure-Local ID"): Index within a single structure
-- Bidirectional mapping enables persistent identity despite structure changes
-
-### Append-Only Storage
-
-- **GeologMeta**: Single homoiconic theory instance storing all data
-- **Patch-based Versioning**: Each commit is a delta from parent
-- **Never Delete**: Elements only tombstoned for perfect audit trails
-
-### Type System
-
-- **Postfix Application**: `x f` not `f(x)` — categorical style
-- **Derived Sorts**: Products of base sorts for record domains
-- **Product Domains**: Functions can take record arguments: `[x: M, y: M] -> M`
-- **Relations → Prop**: Relations are functions to `Prop` (boolean predicates)
-
-### Chase Algorithm
-
-- **Fixpoint Iteration**: Derives all consequences until closure
-- **Congruence Closure Integration**: Merges elements when axioms conclude `x = y`
-- **Termination for Unit Laws**: Categories with unit laws no longer loop forever
-- Uses tensor algebra for efficient axiom checking
-
-### Solver Architecture
-
-- **Explicit Search Tree**: Not implicit in call stack (AI-friendly for agent control)
-- **Refinement Preorder**: Structures can grow (carriers, functions, relations)
-- **Obligations vs Unsat**: Axiom obligation = need to witness conclusion (NOT failure)
-- **True Unsat**: Only when deriving `⊢ False` from instantiated axioms
-- **Tactics-based**: AutoTactic composes multiple tactics
-
-### Relational Algebra Compilation
-
-- **QueryOp Intermediate**: SQL-like operators (Scan, Filter, Join, Project, etc.)
-- **Optimization Passes**: Filter fusion, projection pushdown
-- **Store-aware**: Compiled directly to GeologMeta queries with indexing
-
-### Tensor Algebra for Axiom Checking
-
-- **Sparse Representation**: Roaring Bitmaps for efficient membership
-- **Lazy Expression Trees**: Tensor products fused with contractions
-- **Boolean Semiring**: AND for product, OR for sum
-
----
-
-## REPL Commands
-
-```
-:list, :inspect <name>         - Introspection
-:add, :assert, :retract        - Mutations
-:query, :explain, :compile     - Query analysis
-:chase, :solve, :extend        - Inference
-:commit, :history              - Version control
-:source <file>                 - Load programs
-:help                          - Show help
-```
-
----
-
-## Parameterized Theories
-
-Theories can be parameterized by other instances:
-
-```geolog
-theory (N : PetriNet instance) Marking {
-  token : Sort;
-  token/of : token -> N/P;
-}
-```
-
-This enables rich type-theoretic modeling (e.g., Petri net reachability as dependent types).
-
----
-
-## Testing Infrastructure
-
-- **Property-based tests** (`proptest`): naming, overlay, patches, queries, structure, tensor, universe, solver
-- **Unit tests**: parsing, elaboration, meta, pretty-printing, relations, version control, workspace
-- **Integration tests**: 30+ `.geolog` example files
-- **Fuzzing**: `fuzz/` directory with parser and REPL fuzzing targets
-
----
-
-## Project Status
-
-**Version**: 0.1.0 (Early production)
-
-### Completed
-
-- Core geometric logic implementation
-- Parser, elaborator, and core IR
-- Chase algorithm with equality saturation
-- Solver with SMT-like model enumeration
-- Persistence and version control
-- Comprehensive test coverage
-
-### Active Development
-
-- Nested instance elaboration
-- Homoiconic query plan representation
-- Disjunction variable alignment for tensor builder
-- Lean4 formalization of monotonic submodel proofs
-
----
-
-## Key Files Reference
-
-| File                   | Line Count (approx) | Description           |
-|------------------------|---------------------|-----------------------|
-| `src/core.rs`          | ~800                | Core type definitions |
-| `src/parser.rs`        | ~600                | Parser implementation |
-| `src/repl.rs`          | ~1000               | REPL state machine    |
-| `src/query/chase.rs`   | ~500                | Chase algorithm       |
-| `src/solver/mod.rs`    | ~400                | Model enumeration API |
-| `src/tensor/sparse.rs` | ~600                | Sparse tensor storage |
-| `src/store/mod.rs`     | ~400                | Storage coordination  |

notes/project-completeness-report.md

@@ -1,168 +0,0 @@
-# Geolog Project Completeness Report
-
-*Generated: 2026-03-17*
-
-## Project Overview
-
-**Geolog** is a Geometric Logic REPL and reasoning engine written in Rust. It implements geometric logic with semantics in topoi.
-
-### Key Capabilities
-
-- Define mathematical theories using sorts (types), functions, relations, and axioms
-- Create concrete finite model instances of theories
-- Automatically derive facts using the **chase algorithm** (fixpoint inference)
-- Verify axioms using **tensor algebra** (sparse tensor evaluation)
-- Solve models using SMT-like automated search tactics
-- Version control with git-like commits and persistent append-only storage
-- Interactive REPL for exploration and manipulation
-
-### Use Cases
-
-Business process workflow orchestration, formal verification, database schema definition, Petri net reachability analysis, and diagrammatic rewriting.
-
----
-
-## Current State of Implementation
-
-**Version:** 0.1.0 - Early Production
-
-### Codebase Metrics
-
-| Metric | Count |
-|--------|-------|
-| Rust source code | 30,284 lines |
-| Test code | 7,872 lines |
-| Example `.geolog` files | 2,346 lines |
-| Example files | 30 |
-| Rust source files | 84 |
-| Unit tests | 137 (all passing) |
-| Integration tests | 31 (all passing) |
-
-### Major Implemented Components
-
-1. **Parser** (`src/parser.rs`, `src/lexer.rs`) - Full syntax support via chumsky
-2. **Elaboration** (`src/elaborate/`) - Type checking and AST→Core IR transformation
-3. **Core IR** (`src/core.rs`) - Complete typed representation (Signature, Structure, Formula, Term)
-4. **Chase Algorithm** (`src/query/chase.rs`) - Fixpoint computation with congruence closure for equality saturation
-5. **Tensor Algebra** (`src/tensor/`) - Sparse tensor evaluation for axiom checking
-6. **Solver** (`src/solver/`) - SMT-style model enumeration with multiple tactics
-7. **Storage Layer** (`src/store/`) - Append-only persistent storage with version control
-8. **Query Engine** (`src/query/`) - Relational algebra IR and compilation
-9. **REPL** (`src/repl.rs`) - Full interactive CLI with 20+ commands
-
----
-
-## TODOs, FIXMEs, and Incomplete Features
-
-### Minor TODOs (11 instances)
-
-| Location | Description |
-|----------|-------------|
-| `src/repl.rs:84` | Store full theory_type in GeologMeta for proper reconstruction |
-| `src/overlay.rs:380` | Copy functions (marked as complex, deferred) |
-| `src/store/query.rs:61` | Columnar batch loading for relation tuples |
-| `src/store/bootstrap_queries.rs` | Further integration with query engine |
-| `src/store/instance.rs` | Handle external references, product domains, product codomains |
-| `src/query/to_relalg.rs` | Column path navigation for nested schemas, ScanRelationOp implementation |
-
-### Macro Usage
-
-- 52 instances of `panic!`, `unimplemented!`, `todo!` markers scattered across the codebase
-- Most are used defensively in error paths or for features explicitly deferred
-- Only a small number appear to be in active execution paths
-
-### Active Development Areas
-
-From NOTES.md:
-- Nested instance elaboration (partially done)
-- Homoiconic query plan representation
-- Disjunction variable alignment for tensor builder
-- Lean4 formalization of monotonic submodel proofs
-
----
-
-## Documentation
-
-### Available Documentation
-
-| Document | Description |
-|----------|-------------|
-| **README.md** (1,315 lines) | Comprehensive with quick start, features, showcase (Petri nets), and full examples |
-| **ARCHITECTURE.md** | Detailed module structure, data flow, design principles |
-| **SYNTAX.md** | Complete grammar reference with examples |
-| **NOTES.md** (322 lines) | Technical overview, directory structure, design decisions |
-| **30 example `.geolog` files** | Working demonstrations (graphs, monoids, preorders, Petri nets, categories) |
-
-Documentation quality is **exceptionally high** with clear explanations of complex concepts like geometric logic, chase algorithm, equality saturation, and tensor algebra.
-
----
-
-## Tests and Comprehensiveness
-
-### Test Coverage
-
-- 137 unit tests - All passing
-- 31 integration tests - All passing
-- Property-based tests (proptest): naming, overlay, patches, queries, structure, tensor, universe, solver
-- Fuzzing infrastructure - `fuzz/` directory with parser and REPL fuzzing targets
-- Snapshot testing (insta) - For parsing and elaboration
-
-### Test Files
-
-| File | Coverage Area |
-|------|---------------|
-| `tests/unit_elaborate.rs` | Type checking (14 tests) |
-| `tests/unit_chase.rs` | Chase algorithm (comprehensive) |
-| `tests/unit_parsing.rs` | Parser (4 tests) |
-| `tests/examples_integration.rs` | 31 integration tests covering all examples |
-| `tests/proptest_*.rs` | 11 property-based test suites |
-
-Tests are **comprehensive, well-structured, and demonstrating good coverage** of both core functionality and edge cases.
-
----
-
-## Completeness Assessment
-
-### Complete/Functional
-
-- Core geometric logic engine
-- Parser, lexer, and syntax support
-- Type system and elaboration
-- Chase algorithm with equality saturation
-- Tensor algebra for axiom checking
-- SMT-solver-style model enumeration
-- Persistence and version control
-- Interactive REPL
-- Comprehensive test suite
-
-### Mostly Complete/Production-Ready
-
-- Parameterized theories
-- Nested instances (parsing done, elaboration partial)
-- Query optimization
-- Relational algebra compilation
-- Congruence closure integration
-
-### Minor Gaps/Deferred
-
-- Some advanced columnar batch persistence optimizations
-- External references in instances
-- Product domain handling in some edge cases
-- Complete homoiconic query plan representation
-- Lean4 formalization (work in progress)
-
----
-
-## Conclusion
-
-This project is **substantially complete and production-ready** for its core functionality. It's a sophisticated formal reasoning engine with:
-
-- **Clean architecture** with well-separated concerns
-- **Robust implementation** (30K+ lines of carefully-structured code)
-- **Excellent test coverage** (170+ tests, all passing)
-- **Professional documentation** (README, architecture guides, syntax reference)
-- **Real-world examples** (Petri nets, category theory, preorders, etc.)
-
-The TODOs and FIXMEs are **minor optimizations and edge cases**, not blocking issues. The 61 panic/unimplemented occurrences are mostly defensive error handling or explicitly deferred features, not blocking functionality.
-
-This is a mature, well-tested implementation of a complex formal reasoning system. The "0.1.0" version number likely reflects that the public API may evolve, not that the implementation is immature.

src/bin/geolog-gui.rs

@@ -0,0 +1,134 @@
+//! Geolog GUI - Graphical interface for geometric logic
+//!
+//! Usage: geolog-gui [workspace]
+//!
+//! Provides a graphical interface for:
+//! - Browsing and editing theories and instances
+//! - Visualizing chase execution
+//! - Displaying relation graphs
+
+use std::path::PathBuf;
+
+use eframe::egui;
+
+use geolog::gui::GeologApp;
+
+const VERSION: &str = env!("CARGO_PKG_VERSION");
+
+fn main() -> eframe::Result<()> {
+    // Parse command line arguments
+    let args: Vec<String> = std::env::args().skip(1).collect();
+    let (workspace_path, source_files) = parse_args(&args);
+
+    // Set up native window options
+    let options = eframe::NativeOptions {
+        viewport: egui::ViewportBuilder::default()
+            .with_inner_size([1200.0, 800.0])
+            .with_min_inner_size([800.0, 600.0])
+            .with_title(format!("Geolog v{}", VERSION)),
+        ..Default::default()
+    };
+
+    // Run the application
+    eframe::run_native(
+        "Geolog",
+        options,
+        Box::new(move |cc| {
+            // Set up custom fonts and styles
+            setup_fonts(&cc.egui_ctx);
+
+            // Create the app
+            let mut app = if let Some(path) = workspace_path {
+                GeologApp::with_path(cc, path)
+            } else {
+                GeologApp::new(cc)
+            };
+
+            // Load source files if provided
+            for path in source_files {
+                app.state.load_file(&path);
+                app.state.execute_editor();
+            }
+
+            Ok(Box::new(app))
+        }),
+    )
+}
+
+/// Parse command line arguments
+fn parse_args(args: &[String]) -> (Option<PathBuf>, Vec<PathBuf>) {
+    let mut workspace_path = None;
+    let mut source_files = Vec::new();
+    let mut i = 0;
+
+    while i < args.len() {
+        let arg = &args[i];
+        match arg.as_str() {
+            "-d" | "--dir" => {
+                if i + 1 < args.len() {
+                    workspace_path = Some(PathBuf::from(&args[i + 1]));
+                    i += 2;
+                } else {
+                    eprintln!("Error: -d requires a path argument");
+                    std::process::exit(1);
+                }
+            }
+            "-h" | "--help" => {
+                println!("geolog-gui v{} - Geometric Logic GUI", VERSION);
+                println!();
+                println!("Usage: geolog-gui [OPTIONS] [source_files...]");
+                println!();
+                println!("Options:");
+                println!("  -d, --dir <path>   Use <path> as workspace directory for persistence");
+                println!("  -h, --help         Show this help message");
+                println!("  -v, --version      Show version");
+                println!();
+                println!("Examples:");
+                println!("  geolog-gui                     Start GUI (in-memory, no persistence)");
+                println!("  geolog-gui -d ./myproject      Start GUI with workspace persistence");
+                println!("  geolog-gui file.geolog         Load file.geolog on startup");
+                std::process::exit(0);
+            }
+            "-v" | "--version" => {
+                println!("geolog-gui v{}", VERSION);
+                std::process::exit(0);
+            }
+            _ if arg.starts_with('-') => {
+                eprintln!("Error: Unknown option '{}'", arg);
+                eprintln!("Try 'geolog-gui --help' for usage information");
+                std::process::exit(1);
+            }
+            _ => {
+                // Positional argument - treat as source file
+                source_files.push(PathBuf::from(arg));
+                i += 1;
+            }
+        }
+    }
+
+    (workspace_path, source_files)
+}
+
+/// Set up custom fonts and styles
+fn setup_fonts(ctx: &egui::Context) {
+    // Use a slightly larger default font
+    let mut style = (*ctx.style()).clone();
+    style.text_styles.insert(
+        egui::TextStyle::Body,
+        egui::FontId::proportional(14.0),
+    );
+    style.text_styles.insert(
+        egui::TextStyle::Heading,
+        egui::FontId::proportional(18.0),
+    );
+    style.text_styles.insert(
+        egui::TextStyle::Monospace,
+        egui::FontId::monospace(13.0),
+    );
+
+    // Set up dark theme with custom colors
+    style.visuals = egui::Visuals::dark();
+    style.visuals.override_text_color = Some(egui::Color32::from_gray(220));
+
+    ctx.set_style(style);
+}

src/bin/geolog.rs

@@ -254,6 +254,9 @@ fn handle_command(state: &mut ReplState, cmd: MetaCommand) -> bool {
         MetaCommand::Chase { instance, max_iterations } => {
             handle_chase(state, &instance, max_iterations);
         }
+        MetaCommand::DebugChase { instance, max_iterations } => {
+            handle_debug_chase(state, &instance, max_iterations);
+        }
         MetaCommand::Unknown(msg) => {
             eprintln!("Error: {}", msg);
             eprintln!("Type :help for available commands");
@@ -342,6 +345,7 @@ fn print_help(topic: Option<&str>) {
             println!("  :explain <inst> <sort>      Show query execution plan");
             println!("  :compile <inst> <sort>      Show RelAlgIR compilation");
             println!("  :chase <inst> [max_iter]    Run chase on instance axioms");
+            println!("  :debug-chase <inst> [max]   Run chase with interactive debugger");
             println!();
             println!("Solver:");
             println!("  :solve <theory> [budget_ms]          Find model of theory from scratch");
@@ -1078,6 +1082,102 @@ fn handle_chase(state: &mut ReplState, instance_name: &str, max_iterations: Opti
     }
 }
 
+/// Handle :debug-chase command - run chase with interactive debugger
+fn handle_debug_chase(state: &mut ReplState, instance_name: &str, max_iterations: Option<usize>) {
+    use geolog::core::RelationStorage;
+    use geolog::debugger::InteractiveDebugger;
+    use geolog::query::chase::chase_fixpoint_with_observer;
+
+    // Get the instance
+    let entry = match state.instances.get_mut(instance_name) {
+        Some(e) => e,
+        None => {
+            eprintln!("Instance '{}' not found", instance_name);
+            return;
+        }
+    };
+
+    // Get the theory
+    let theory = match state.theories.get(&entry.theory_name) {
+        Some(t) => t.clone(),
+        None => {
+            eprintln!("Theory '{}' not found", entry.theory_name);
+            return;
+        }
+    };
+
+    let sig = &theory.theory.signature;
+    let axioms = &theory.theory.axioms;
+    let axiom_names = &theory.theory.axiom_names;
+
+    if axioms.is_empty() {
+        println!("Theory '{}' has no axioms to chase.", entry.theory_name);
+        return;
+    }
+
+    println!("Starting debug chase on instance '{}' (theory '{}')", instance_name, entry.theory_name);
+    println!("{} axiom(s) to process", axioms.len());
+    println!("Type 'help' for debugger commands.\n");
+
+    // Snapshot relation tuple counts before chase
+    let tuple_counts_before: Vec<usize> = entry.structure.relations
+        .iter()
+        .map(|r| r.len())
+        .collect();
+
+    // Create debugger with element name mapping
+    let mut debugger = InteractiveDebugger::new(&entry.slid_to_name, axiom_names);
+
+    // Run the chase with observer
+    let max_iter = max_iterations.unwrap_or(100);
+
+    match chase_fixpoint_with_observer(
+        axioms,
+        axiom_names,
+        &mut entry.structure,
+        &mut state.store.universe,
+        sig,
+        max_iter,
+        &mut debugger,
+    ) {
+        Ok(iterations) => {
+            println!("\nStructure after chase:");
+            print_structure_summary(&entry.structure, sig);
+
+            // Check if any new tuples were added
+            let tuple_counts_after: Vec<usize> = entry.structure.relations
+                .iter()
+                .map(|r| r.len())
+                .collect();
+            let tuples_added = tuple_counts_before.iter()
+                .zip(tuple_counts_after.iter())
+                .any(|(before, after)| after > before);
+
+            // Save info needed for persistence before dropping entry borrow
+            let theory_name_owned = entry.theory_name.clone();
+
+            if tuples_added {
+                if let Err(e) = persist_chase_results(
+                    state,
+                    instance_name,
+                    &theory_name_owned,
+                ) {
+                    eprintln!("Warning: Failed to persist chase results: {}", e);
+                } else {
+                    println!("Chase results persisted to store.");
+                }
+            }
+
+            if iterations == 0 {
+                println!("\nChase stopped by user.");
+            }
+        }
+        Err(e) => {
+            eprintln!("✗ Chase error: {}", e);
+        }
+    }
+}
+
 /// Persist chase results (relation tuples) to columnar batches as IDB data.
 ///
 /// IDB batches are persisted locally but NOT transmitted over the wire.

src/debugger.rs

@@ -0,0 +1,291 @@
+//! Interactive debugger for the chase algorithm.
+//!
+//! Provides step-through debugging, breakpoints, and variable inspection
+//! for understanding chase execution.
+
+use std::collections::{HashMap, HashSet};
+use std::io::{self, Write};
+
+use crate::id::Slid;
+use crate::query::chase::{Binding, ChaseControl, ChaseEvent, ChaseObserver};
+
+/// Debug mode controlling execution flow
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum DebugMode {
+    /// Continue until breakpoint or completion
+    Continue,
+    /// Step to next axiom firing
+    Step,
+    /// Step to next iteration
+    StepIteration,
+}
+
+/// Interactive debugger for chase execution
+pub struct InteractiveDebugger<'a> {
+    /// Current debug mode
+    mode: DebugMode,
+    /// Breakpoints on axiom name patterns
+    breakpoints: HashSet<String>,
+    /// Mapping from Slid to element names for display
+    slid_to_name: &'a HashMap<Slid, String>,
+    /// Last binding seen (for inspect command)
+    last_binding: Option<Binding>,
+    /// Axiom names for display
+    axiom_names: &'a [String],
+    /// Current iteration number
+    current_iteration: usize,
+    /// Whether we should stop (user quit)
+    should_stop: bool,
+}
+
+impl<'a> InteractiveDebugger<'a> {
+    /// Create a new interactive debugger
+    pub fn new(
+        slid_to_name: &'a HashMap<Slid, String>,
+        axiom_names: &'a [String],
+    ) -> Self {
+        Self {
+            mode: DebugMode::Step, // Start in step mode
+            breakpoints: HashSet::new(),
+            slid_to_name,
+            last_binding: None,
+            axiom_names,
+            current_iteration: 0,
+            should_stop: false,
+        }
+    }
+
+    /// Format a binding for display using element names
+    pub fn format_binding(&self, binding: &Binding) -> String {
+        if binding.is_empty() {
+            return "(empty)".to_string();
+        }
+
+        let mut parts: Vec<String> = binding
+            .iter()
+            .map(|(var, slid)| {
+                let elem_name = self
+                    .slid_to_name
+                    .get(slid)
+                    .map(|s| s.as_str())
+                    .unwrap_or_else(|| "?");
+                format!("{}={}", var, elem_name)
+            })
+            .collect();
+        parts.sort(); // Consistent ordering
+        parts.join(", ")
+    }
+
+    /// Check if an axiom name matches any breakpoint pattern
+    fn matches_breakpoint(&self, axiom_name: Option<&str>) -> bool {
+        let Some(name) = axiom_name else {
+            return false;
+        };
+
+        self.breakpoints.iter().any(|pattern| {
+            // Simple substring matching for now
+            name.contains(pattern)
+        })
+    }
+
+    /// Process a debugger command
+    fn process_command(&mut self, cmd: &str) -> bool {
+        let parts: Vec<&str> = cmd.trim().split_whitespace().collect();
+        let command = parts.first().map(|s| *s).unwrap_or("");
+
+        match command {
+            "s" | "step" => {
+                self.mode = DebugMode::Step;
+                true // Continue execution
+            }
+            "c" | "continue" => {
+                self.mode = DebugMode::Continue;
+                true
+            }
+            "n" | "next" => {
+                self.mode = DebugMode::StepIteration;
+                true
+            }
+            "b" | "break" => {
+                if let Some(pattern) = parts.get(1) {
+                    self.breakpoints.insert(pattern.to_string());
+                    println!("Breakpoint set on axioms matching '{}'", pattern);
+                } else {
+                    println!("Usage: break <pattern>");
+                }
+                false // Don't continue, wait for another command
+            }
+            "d" | "delete" => {
+                if let Some(pattern) = parts.get(1) {
+                    if self.breakpoints.remove(*pattern) {
+                        println!("Breakpoint '{}' removed", pattern);
+                    } else {
+                        println!("No breakpoint matching '{}'", pattern);
+                    }
+                } else {
+                    self.breakpoints.clear();
+                    println!("All breakpoints cleared");
+                }
+                false
+            }
+            "i" | "inspect" => {
+                if let Some(binding) = &self.last_binding {
+                    println!("Current binding: {}", self.format_binding(binding));
+                } else {
+                    println!("No binding available");
+                }
+                false
+            }
+            "l" | "list" => {
+                if self.breakpoints.is_empty() {
+                    println!("No breakpoints set");
+                } else {
+                    println!("Breakpoints:");
+                    for bp in &self.breakpoints {
+                        println!("  - {}", bp);
+                    }
+                }
+                println!("\nAxioms:");
+                for (i, name) in self.axiom_names.iter().enumerate() {
+                    let display_name = if name.is_empty() { "(unnamed)" } else { name.as_str() };
+                    println!("  #{}: {}", i, display_name);
+                }
+                false
+            }
+            "q" | "quit" => {
+                self.should_stop = true;
+                true
+            }
+            "h" | "help" | "?" => {
+                print_help();
+                false
+            }
+            "" => false, // Empty line, just reprompt
+            _ => {
+                println!("Unknown command: '{}'. Type 'help' for available commands.", command);
+                false
+            }
+        }
+    }
+
+    /// Wait for user input and process commands
+    fn prompt(&mut self) -> ChaseControl {
+        loop {
+            print!("(chase-dbg) ");
+            io::stdout().flush().ok();
+
+            let mut input = String::new();
+            if io::stdin().read_line(&mut input).is_err() {
+                self.should_stop = true;
+                return ChaseControl::Stop;
+            }
+
+            let should_continue = self.process_command(&input);
+
+            if self.should_stop {
+                return ChaseControl::Stop;
+            }
+
+            if should_continue {
+                return ChaseControl::Continue;
+            }
+        }
+    }
+}
+
+impl<'a> ChaseObserver for InteractiveDebugger<'a> {
+    fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl {
+        if self.should_stop {
+            return ChaseControl::Stop;
+        }
+
+        match event {
+            ChaseEvent::IterationStart { iteration } => {
+                self.current_iteration = iteration;
+                println!("\n--- Iteration {} ---", iteration);
+                ChaseControl::Continue
+            }
+
+            ChaseEvent::AxiomFiring {
+                axiom_index,
+                axiom_name,
+                binding,
+                violation_count,
+            } => {
+                // Store binding for inspect command
+                self.last_binding = Some(binding.clone());
+
+                let name_display = axiom_name.unwrap_or("(unnamed)");
+                println!(
+                    "Firing axiom #{}: {} ({} violations)",
+                    axiom_index, name_display, violation_count
+                );
+                println!("  Binding: {}", self.format_binding(binding));
+
+                // Check if we should stop
+                let should_prompt = match self.mode {
+                    DebugMode::Step => true,
+                    DebugMode::Continue => self.matches_breakpoint(axiom_name),
+                    DebugMode::StepIteration => false,
+                };
+
+                if should_prompt {
+                    if self.matches_breakpoint(axiom_name) {
+                        println!("  [Breakpoint hit]");
+                    }
+                    self.prompt()
+                } else {
+                    ChaseControl::Continue
+                }
+            }
+
+            ChaseEvent::AxiomFired {
+                axiom_index: _,
+                axiom_name: _,
+                changed,
+            } => {
+                if changed {
+                    println!("  -> Structure changed");
+                }
+                ChaseControl::Continue
+            }
+
+            ChaseEvent::IterationEnd {
+                iteration,
+                changed,
+            } => {
+                if !changed {
+                    println!("Iteration {} complete (no changes - fixpoint reached)", iteration);
+                } else {
+                    println!("Iteration {} complete (structure changed)", iteration);
+                }
+
+                // In StepIteration mode, prompt at end of iteration
+                if self.mode == DebugMode::StepIteration {
+                    self.prompt()
+                } else {
+                    ChaseControl::Continue
+                }
+            }
+
+            ChaseEvent::ChaseComplete { iterations } => {
+                println!("\nChase complete after {} iterations.", iterations);
+                ChaseControl::Continue
+            }
+        }
+    }
+}
+
+fn print_help() {
+    println!("Chase Debugger Commands:");
+    println!();
+    println!("  step, s        Step to next axiom firing");
+    println!("  continue, c    Continue until breakpoint or completion");
+    println!("  next, n        Step to next iteration");
+    println!("  break <pat>, b Set breakpoint on axioms matching pattern");
+    println!("  delete [pat], d  Remove breakpoint (all if no pattern)");
+    println!("  inspect, i     Show current variable binding");
+    println!("  list, l        List breakpoints and axioms");
+    println!("  quit, q        Stop the chase");
+    println!("  help, h, ?     Show this help");
+}

src/gui/app.rs

@@ -0,0 +1,408 @@
+//! Main Geolog GUI application
+//!
+//! Implements the egui::App trait for the main application window.
+
+use eframe::egui;
+use std::path::PathBuf;
+
+use super::panels::{BrowserPanel, ConsolePanel, EditorPanel, InspectorPanel};
+use super::state::{CentralView, GuiState};
+use super::visualizations::{ChaseVisualization, GraphView};
+
+/// Main Geolog GUI application
+pub struct GeologApp {
+    /// Application state
+    pub state: GuiState,
+
+    /// Panel instances
+    browser: BrowserPanel,
+    editor: EditorPanel,
+    inspector: InspectorPanel,
+    console: ConsolePanel,
+    chase_viz: ChaseVisualization,
+    graph_view: GraphView,
+
+    /// Editor/Inspector split ratio (0.0 to 1.0, where 0.5 = equal)
+    editor_split: f32,
+}
+
+impl GeologApp {
+    /// Create a new Geolog application
+    pub fn new(_cc: &eframe::CreationContext<'_>) -> Self {
+        Self {
+            state: GuiState::new(),
+            browser: BrowserPanel::new(),
+            editor: EditorPanel::new(),
+            inspector: InspectorPanel::new(),
+            console: ConsolePanel::new(),
+            chase_viz: ChaseVisualization::new(),
+            graph_view: GraphView::new(),
+            editor_split: 0.5, // 50% editor, 50% inspector
+        }
+    }
+
+    /// Create a new application with a workspace path
+    pub fn with_path(_cc: &eframe::CreationContext<'_>, path: PathBuf) -> Self {
+        let mut app = Self::new(_cc);
+        app.state = GuiState::with_path(path);
+        app
+    }
+
+    /// Render the menu bar
+    fn menu_bar(&mut self, ui: &mut egui::Ui) {
+        egui::menu::bar(ui, |ui| {
+            ui.menu_button("File", |ui| {
+                if ui.button("Open...").clicked() {
+                    self.handle_open_file();
+                    ui.close_menu();
+                }
+                if ui.button("Save").clicked() {
+                    self.handle_save_file();
+                    ui.close_menu();
+                }
+                ui.separator();
+                if ui.button("Reset State").clicked() {
+                    self.state.repl.reset();
+                    self.state.log_info("State reset");
+                    ui.close_menu();
+                }
+                ui.separator();
+                if ui.button("Quit").clicked() {
+                    std::process::exit(0);
+                }
+            });
+
+            ui.menu_button("Edit", |ui| {
+                if ui.button("Clear Editor").clicked() {
+                    self.state.editor_content.clear();
+                    ui.close_menu();
+                }
+                if ui.button("Clear Console").clicked() {
+                    self.state.clear_console();
+                    ui.close_menu();
+                }
+            });
+
+            ui.menu_button("View", |ui| {
+                if ui
+                    .selectable_label(
+                        self.state.central_view == CentralView::EditorAndInspector,
+                        "Editor & Inspector",
+                    )
+                    .clicked()
+                {
+                    self.state.central_view = CentralView::EditorAndInspector;
+                    ui.close_menu();
+                }
+                if ui
+                    .selectable_label(
+                        self.state.central_view == CentralView::ChaseVisualization,
+                        "Chase Visualization",
+                    )
+                    .clicked()
+                {
+                    self.state.central_view = CentralView::ChaseVisualization;
+                    ui.close_menu();
+                }
+                if ui
+                    .selectable_label(
+                        self.state.central_view == CentralView::GraphVisualization,
+                        "Graph Visualization",
+                    )
+                    .clicked()
+                {
+                    self.state.central_view = CentralView::GraphVisualization;
+                    ui.close_menu();
+                }
+            });
+
+            ui.menu_button("Chase", |ui| {
+                if let Some(crate::gui::state::SelectedItem::Instance(name)) =
+                    &self.state.selected_item
+                {
+                    let name = name.clone();
+                    if ui.button(format!("Run Chase on {}", name)).clicked() {
+                        self.handle_run_chase(&name);
+                        ui.close_menu();
+                    }
+                    if ui.button(format!("Debug Chase on {}", name)).clicked() {
+                        self.state.start_chase(&name);
+                        ui.close_menu();
+                    }
+                } else {
+                    ui.label("(Select an instance first)");
+                }
+            });
+
+            ui.menu_button("Help", |ui| {
+                if ui.button("About").clicked() {
+                    self.state.log_info(format!(
+                        "Geolog GUI v{}",
+                        env!("CARGO_PKG_VERSION")
+                    ));
+                    ui.close_menu();
+                }
+                if ui.button("Syntax Help").clicked() {
+                    self.show_syntax_help();
+                    ui.close_menu();
+                }
+            });
+        });
+    }
+
+    /// Handle opening a file
+    fn handle_open_file(&mut self) {
+        if let Some(path) = rfd::FileDialog::new()
+            .add_filter("Geolog", &["geolog"])
+            .add_filter("All Files", &["*"])
+            .pick_file()
+        {
+            self.state.load_file(&path);
+        }
+    }
+
+    /// Handle saving a file
+    fn handle_save_file(&mut self) {
+        if let Some(path) = &self.state.current_file {
+            match std::fs::write(path, &self.state.editor_content) {
+                Ok(()) => {
+                    self.state.log_success(format!("Saved: {}", path.display()));
+                }
+                Err(e) => {
+                    self.state.log_error(format!("Failed to save: {}", e));
+                }
+            }
+        } else {
+            // Save As
+            if let Some(path) = rfd::FileDialog::new()
+                .add_filter("Geolog", &["geolog"])
+                .save_file()
+            {
+                match std::fs::write(&path, &self.state.editor_content) {
+                    Ok(()) => {
+                        self.state.current_file = Some(path.clone());
+                        self.state.log_success(format!("Saved: {}", path.display()));
+                    }
+                    Err(e) => {
+                        self.state.log_error(format!("Failed to save: {}", e));
+                    }
+                }
+            }
+        }
+    }
+
+    /// Run chase on an instance
+    fn handle_run_chase(&mut self, instance_name: &str) {
+        use crate::core::RelationStorage;
+        use crate::query::chase::chase_fixpoint;
+
+        // Get theory name first (immutable borrow)
+        let theory_name = match self.state.repl.instances.get(instance_name) {
+            Some(e) => e.theory_name.clone(),
+            None => {
+                self.state
+                    .log_error(format!("Instance '{}' not found", instance_name));
+                return;
+            }
+        };
+
+        let theory = match self.state.repl.theories.get(&theory_name) {
+            Some(t) => t.clone(),
+            None => {
+                self.state
+                    .log_error(format!("Theory '{}' not found", theory_name));
+                return;
+            }
+        };
+
+        let sig = &theory.theory.signature;
+        let axioms = &theory.theory.axioms;
+
+        if axioms.is_empty() {
+            self.state
+                .log_warning(format!("Theory '{}' has no axioms to chase", theory_name));
+            return;
+        }
+
+        self.state.log_info(format!(
+            "Running chase on instance '{}' ({} axioms)...",
+            instance_name,
+            axioms.len()
+        ));
+
+        // Now get mutable access to entry
+        let entry = self.state.repl.instances.get_mut(instance_name).unwrap();
+
+        let start = std::time::Instant::now();
+        let result = chase_fixpoint(
+            axioms,
+            &mut entry.structure,
+            &mut self.state.repl.store.universe,
+            sig,
+            100,
+        );
+
+        match result {
+            Ok(iterations) => {
+                let elapsed = start.elapsed();
+                // Get structure info before releasing borrow
+                let total_tuples: usize =
+                    entry.structure.relations.iter().map(|r| r.len()).sum();
+                let num_elements = entry.structure.len();
+
+                self.state.log_success(format!(
+                    "Chase completed in {} iterations ({:.2}ms)",
+                    iterations,
+                    elapsed.as_secs_f64() * 1000.0
+                ));
+
+                // Show structure summary
+                self.state.log_info(format!(
+                    "Structure: {} elements, {} relation tuples",
+                    num_elements,
+                    total_tuples
+                ));
+            }
+            Err(e) => {
+                self.state.log_error(format!("Chase error: {}", e));
+            }
+        }
+    }
+
+    /// Show syntax help in the console
+    fn show_syntax_help(&mut self) {
+        self.state.log_info("=== Geolog Syntax ===");
+        self.state.log_info("");
+        self.state.log_info("theory Name {");
+        self.state.log_info("  Sort1 : Sort;");
+        self.state.log_info("  func : Sort1 -> Sort2;");
+        self.state.log_info("  rel : Sort1 -> Prop;");
+        self.state.log_info("}");
+        self.state.log_info("");
+        self.state.log_info("instance Name : Theory = {");
+        self.state.log_info("  elem : Sort1;");
+        self.state.log_info("  elem func = other_elem;");
+        self.state.log_info("  elem rel;");
+        self.state.log_info("}");
+    }
+
+    /// Render the central panel based on current view mode
+    fn central_panel(&mut self, ui: &mut egui::Ui) {
+        match self.state.central_view {
+            CentralView::EditorAndInspector => {
+                // Split vertically: editor on top, inspector on bottom
+                let available_height = ui.available_height();
+                let splitter_height = 8.0;
+                // Ensure heights are never negative
+                let usable_height = (available_height - splitter_height).max(0.0);
+                let editor_height = (usable_height * self.editor_split).max(0.0);
+                let inspector_height = (usable_height * (1.0 - self.editor_split)).max(0.0);
+
+                // Editor section
+                ui.allocate_ui_with_layout(
+                    egui::vec2(ui.available_width(), editor_height),
+                    egui::Layout::top_down(egui::Align::LEFT),
+                    |ui| {
+                        self.editor.show(ui, &mut self.state);
+                    },
+                );
+
+                // Draggable splitter
+                let splitter_response = ui.allocate_response(
+                    egui::vec2(ui.available_width(), splitter_height),
+                    egui::Sense::drag(),
+                );
+
+                // Draw splitter bar
+                let splitter_rect = splitter_response.rect;
+                let is_dragging = splitter_response.dragged();
+                let is_hovered = splitter_response.hovered();
+
+                let splitter_color = if is_dragging {
+                    egui::Color32::from_rgb(100, 150, 255)
+                } else if is_hovered {
+                    egui::Color32::from_rgb(80, 80, 100)
+                } else {
+                    egui::Color32::from_rgb(60, 60, 70)
+                };
+
+                ui.painter().rect_filled(splitter_rect, 0.0, splitter_color);
+
+                // Draw grip lines
+                let center_y = splitter_rect.center().y;
+                let grip_width = 30.0;
+                let grip_x = splitter_rect.center().x;
+                for i in -1..=1 {
+                    let y = center_y + (i as f32) * 2.0;
+                    ui.painter().line_segment(
+                        [
+                            egui::pos2(grip_x - grip_width / 2.0, y),
+                            egui::pos2(grip_x + grip_width / 2.0, y),
+                        ],
+                        egui::Stroke::new(1.0, egui::Color32::GRAY),
+                    );
+                }
+
+                // Handle dragging
+                if is_dragging {
+                    let delta = splitter_response.drag_delta().y;
+                    let divisor = (available_height - splitter_height).max(1.0);
+                    let new_split = self.editor_split + delta / divisor;
+                    self.editor_split = new_split.clamp(0.1, 0.9);
+                }
+
+                // Change cursor when hovering
+                if is_hovered || is_dragging {
+                    ui.ctx().set_cursor_icon(egui::CursorIcon::ResizeVertical);
+                }
+
+                // Inspector section
+                ui.allocate_ui_with_layout(
+                    egui::vec2(ui.available_width(), inspector_height),
+                    egui::Layout::top_down(egui::Align::LEFT),
+                    |ui| {
+                        self.inspector.show(ui, &mut self.state);
+                    },
+                );
+            }
+            CentralView::ChaseVisualization => {
+                self.chase_viz.show(ui, &mut self.state);
+            }
+            CentralView::GraphVisualization => {
+                self.graph_view.show(ui, &mut self.state);
+            }
+        }
+    }
+}
+
+impl eframe::App for GeologApp {
+    fn update(&mut self, ctx: &egui::Context, _frame: &mut eframe::Frame) {
+        // Top menu bar
+        egui::TopBottomPanel::top("menu_bar").show(ctx, |ui| {
+            self.menu_bar(ui);
+        });
+
+        // Left panel: Browser
+        egui::SidePanel::left("browser_panel")
+            .default_width(200.0)
+            .min_width(150.0)
+            .resizable(true)
+            .show(ctx, |ui| {
+                self.browser.show(ui, &mut self.state);
+            });
+
+        // Bottom panel: Console
+        egui::TopBottomPanel::bottom("console_panel")
+            .default_height(150.0)
+            .min_height(100.0)
+            .resizable(true)
+            .show(ctx, |ui| {
+                self.console.show(ui, &mut self.state);
+            });
+
+        // Central panel: Editor + Inspector or Visualizations
+        egui::CentralPanel::default().show(ctx, |ui| {
+            self.central_panel(ui);
+        });
+    }
+}

src/gui/mod.rs

@@ -0,0 +1,15 @@
+//! GUI module for Geolog using egui
+//!
+//! Provides a graphical interface for:
+//! - Browsing theories and instances
+//! - Editing geolog code
+//! - Visualizing chase execution
+//! - Displaying relation graphs
+
+pub mod app;
+pub mod panels;
+pub mod state;
+pub mod visualizations;
+
+pub use app::GeologApp;
+pub use state::GuiState;

src/gui/panels/browser.rs

@@ -0,0 +1,178 @@
+//! Browser panel for theory/instance navigation
+//!
+//! Displays a tree view of all theories and instances.
+
+use eframe::egui;
+
+use crate::gui::state::{GuiState, SelectedItem};
+
+/// Browser panel for navigating theories and instances
+pub struct BrowserPanel {
+    /// Search/filter text
+    filter: String,
+}
+
+impl BrowserPanel {
+    pub fn new() -> Self {
+        Self {
+            filter: String::new(),
+        }
+    }
+
+    pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        ui.heading("Browser");
+        ui.separator();
+
+        // Filter input
+        ui.horizontal(|ui| {
+            ui.label("Filter:");
+            ui.text_edit_singleline(&mut self.filter);
+        });
+        ui.add_space(4.0);
+
+        // Scrollable tree view
+        egui::ScrollArea::vertical()
+            .auto_shrink([false, false])
+            .show(ui, |ui| {
+                self.show_theories_section(ui, state);
+                ui.add_space(8.0);
+                self.show_instances_section(ui, state);
+            });
+    }
+
+    fn show_theories_section(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        let theories = state.repl.list_theories();
+        let filtered: Vec<_> = theories
+            .iter()
+            .filter(|t| {
+                self.filter.is_empty()
+                    || t.name.to_lowercase().contains(&self.filter.to_lowercase())
+            })
+            .collect();
+
+        let header = if self.filter.is_empty() {
+            format!("Theories ({})", theories.len())
+        } else {
+            format!("Theories ({}/{})", filtered.len(), theories.len())
+        };
+
+        let response = egui::CollapsingHeader::new(header)
+            .default_open(state.theories_expanded)
+            .show(ui, |ui| {
+                if filtered.is_empty() {
+                    ui.label("(none)");
+                } else {
+                    for theory in filtered {
+                        let is_selected = matches!(
+                            &state.selected_item,
+                            Some(SelectedItem::Theory(name)) if name == &theory.name
+                        );
+
+                        let label = format!(
+                            "{} ({} sorts{}{}{})",
+                            theory.name,
+                            theory.num_sorts,
+                            if theory.num_functions > 0 {
+                                format!(", {} funcs", theory.num_functions)
+                            } else {
+                                String::new()
+                            },
+                            if theory.num_relations > 0 {
+                                format!(", {} rels", theory.num_relations)
+                            } else {
+                                String::new()
+                            },
+                            if theory.num_axioms > 0 {
+                                format!(", {} axioms", theory.num_axioms)
+                            } else {
+                                String::new()
+                            },
+                        );
+
+                        if ui.selectable_label(is_selected, label).clicked() {
+                            state.selected_item = Some(SelectedItem::Theory(theory.name.clone()));
+                        }
+                    }
+                }
+            });
+        state.theories_expanded = response.fully_open();
+    }
+
+    fn show_instances_section(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        let instances = state.repl.list_instances();
+        let filtered: Vec<_> = instances
+            .iter()
+            .filter(|i| {
+                self.filter.is_empty()
+                    || i.name.to_lowercase().contains(&self.filter.to_lowercase())
+                    || i.theory_name
+                        .to_lowercase()
+                        .contains(&self.filter.to_lowercase())
+            })
+            .collect();
+
+        let header = if self.filter.is_empty() {
+            format!("Instances ({})", instances.len())
+        } else {
+            format!("Instances ({}/{})", filtered.len(), instances.len())
+        };
+
+        let response = egui::CollapsingHeader::new(header)
+            .default_open(state.instances_expanded)
+            .show(ui, |ui| {
+                if filtered.is_empty() {
+                    ui.label("(none)");
+                } else {
+                    for instance in filtered {
+                        let is_selected = matches!(
+                            &state.selected_item,
+                            Some(SelectedItem::Instance(name)) if name == &instance.name
+                        );
+
+                        let label = format!(
+                            "{} : {} ({} elems)",
+                            instance.name, instance.theory_name, instance.num_elements
+                        );
+
+                        let response = ui.selectable_label(is_selected, label);
+
+                        // Left click to select
+                        if response.clicked() {
+                            state.selected_item =
+                                Some(SelectedItem::Instance(instance.name.clone()));
+                        }
+
+                        // Right-click context menu
+                        response.context_menu(|ui| {
+                            if ui.button("Inspect").clicked() {
+                                state.selected_item =
+                                    Some(SelectedItem::Instance(instance.name.clone()));
+                                ui.close_menu();
+                            }
+                            if ui.button("Run Chase").clicked() {
+                                // This will be handled by the app
+                                state.selected_item =
+                                    Some(SelectedItem::Instance(instance.name.clone()));
+                                state.log_info(format!(
+                                    "Use Chase menu to run chase on '{}'",
+                                    instance.name
+                                ));
+                                ui.close_menu();
+                            }
+                            if ui.button("View Graph").clicked() {
+                                state.show_graph(&instance.name, None);
+                                ui.close_menu();
+                            }
+                        });
+                    }
+                }
+            });
+        state.instances_expanded = response.fully_open();
+    }
+}
+
+impl Default for BrowserPanel {
+    fn default() -> Self {
+        Self::new()
+    }
+}

src/gui/panels/console.rs

@@ -0,0 +1,412 @@
+//! Console panel for displaying output and error messages
+//!
+//! Shows a scrollable log of messages with color coding and a REPL input.
+
+use eframe::egui;
+
+use crate::gui::state::{GuiState, MessageKind};
+use crate::repl::{MetaCommand, ListTarget, ExecuteResult};
+
+/// Console panel for output messages and REPL input
+pub struct ConsolePanel {
+    /// Whether to auto-scroll to bottom
+    auto_scroll: bool,
+    /// REPL input buffer
+    input: String,
+    /// Command history
+    history: Vec<String>,
+    /// Current position in history (for up/down navigation)
+    history_pos: Option<usize>,
+}
+
+impl ConsolePanel {
+    pub fn new() -> Self {
+        Self {
+            auto_scroll: true,
+            input: String::new(),
+            history: Vec::new(),
+            history_pos: None,
+        }
+    }
+
+    pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Header with title and buttons
+        ui.horizontal(|ui| {
+            ui.heading("Console");
+
+            ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
+                if ui.button("Clear").clicked() {
+                    state.clear_console();
+                }
+
+                ui.checkbox(&mut self.auto_scroll, "Auto-scroll");
+
+                ui.label(format!("{} messages", state.console_messages.len()));
+            });
+        });
+
+        ui.separator();
+
+        // Scrollable message area (takes most of the space)
+        let available_height = (ui.available_height() - 30.0).max(50.0); // Reserve space for input
+        let scroll_area = egui::ScrollArea::vertical()
+            .auto_shrink([false, false])
+            .max_height(available_height)
+            .stick_to_bottom(self.auto_scroll);
+
+        scroll_area.show(ui, |ui| {
+            if state.console_messages.is_empty() {
+                ui.label("Type commands below (e.g., :help, :list, or geolog code)");
+            } else {
+                for message in &state.console_messages {
+                    let color = match message.kind {
+                        MessageKind::Info => egui::Color32::LIGHT_GRAY,
+                        MessageKind::Success => egui::Color32::from_rgb(100, 200, 100),
+                        MessageKind::Error => egui::Color32::from_rgb(255, 100, 100),
+                        MessageKind::Warning => egui::Color32::from_rgb(255, 200, 100),
+                    };
+
+                    let prefix = match message.kind {
+                        MessageKind::Info => ">",
+                        MessageKind::Success => "+",
+                        MessageKind::Error => "!",
+                        MessageKind::Warning => "?",
+                    };
+
+                    ui.horizontal(|ui| {
+                        ui.label(
+                            egui::RichText::new(prefix)
+                                .color(color)
+                                .monospace(),
+                        );
+                        ui.label(
+                            egui::RichText::new(&message.text)
+                                .color(color)
+                                .monospace(),
+                        );
+                    });
+                }
+            }
+        });
+
+        // REPL input at the bottom
+        ui.separator();
+        ui.horizontal(|ui| {
+            ui.label(
+                egui::RichText::new("geolog>")
+                    .monospace()
+                    .color(egui::Color32::from_rgb(100, 150, 255)),
+            );
+
+            let response = ui.add(
+                egui::TextEdit::singleline(&mut self.input)
+                    .font(egui::FontId::monospace(13.0))
+                    .desired_width((ui.available_width() - 60.0).max(50.0))
+                    .hint_text(":help for commands"),
+            );
+
+            // Handle Enter key
+            if response.lost_focus() && ui.input(|i| i.key_pressed(egui::Key::Enter)) {
+                self.execute_input(state);
+                response.request_focus();
+            }
+
+            // Handle Up/Down for history
+            if response.has_focus() {
+                if ui.input(|i| i.key_pressed(egui::Key::ArrowUp)) {
+                    self.history_up();
+                }
+                if ui.input(|i| i.key_pressed(egui::Key::ArrowDown)) {
+                    self.history_down();
+                }
+            }
+
+            if ui.button("Run").clicked() {
+                self.execute_input(state);
+            }
+        });
+    }
+
+    fn execute_input(&mut self, state: &mut GuiState) {
+        let input = self.input.trim().to_string();
+        if input.is_empty() {
+            return;
+        }
+
+        // Add to history
+        self.history.push(input.clone());
+        self.history_pos = None;
+
+        // Echo the input
+        state.log_info(format!("geolog> {}", input));
+
+        // Process the input
+        if input.starts_with(':') {
+            // Meta command
+            let cmd = MetaCommand::parse(&input);
+            self.handle_meta_command(state, cmd);
+        } else {
+            // Geolog code
+            match state.repl.execute_geolog(&input) {
+                Ok(results) => {
+                    for result in results {
+                        match result {
+                            ExecuteResult::Namespace(name) => {
+                                state.log_info(format!("Namespace: {}", name));
+                            }
+                            ExecuteResult::Theory {
+                                name,
+                                num_sorts,
+                                num_functions,
+                                num_relations,
+                                num_axioms,
+                            } => {
+                                let mut parts = vec![format!("{} sorts", num_sorts)];
+                                if num_functions > 0 {
+                                    parts.push(format!("{} functions", num_functions));
+                                }
+                                if num_relations > 0 {
+                                    parts.push(format!("{} relations", num_relations));
+                                }
+                                if num_axioms > 0 {
+                                    parts.push(format!("{} axioms", num_axioms));
+                                }
+                                state.log_success(format!(
+                                    "Defined theory {} ({})",
+                                    name,
+                                    parts.join(", ")
+                                ));
+                            }
+                            ExecuteResult::Instance {
+                                name,
+                                theory_name,
+                                num_elements,
+                            } => {
+                                state.log_success(format!(
+                                    "Defined instance {} : {} ({} elements)",
+                                    name, theory_name, num_elements
+                                ));
+                            }
+                            ExecuteResult::Query(_) => {
+                                state.log_info("Query executed");
+                            }
+                        }
+                    }
+                }
+                Err(e) => {
+                    state.log_error(e);
+                }
+            }
+        }
+
+        self.input.clear();
+    }
+
+    fn handle_meta_command(&mut self, state: &mut GuiState, cmd: MetaCommand) {
+        match cmd {
+            MetaCommand::Help(topic) => {
+                match topic.as_deref() {
+                    None => {
+                        state.log_info("Commands:");
+                        state.log_info("  :help          Show this help");
+                        state.log_info("  :list          List theories and instances");
+                        state.log_info("  :inspect <n>   Inspect a theory or instance");
+                        state.log_info("  :chase <inst>  Run chase on instance");
+                        state.log_info("  :reset         Reset all state");
+                        state.log_info("  :clear         Clear console");
+                        state.log_info("");
+                        state.log_info("Or type geolog code directly.");
+                    }
+                    Some(t) => {
+                        state.log_info(format!("Help topic: {}", t));
+                    }
+                }
+            }
+            MetaCommand::List(target) => {
+                match target {
+                    ListTarget::Theories | ListTarget::All => {
+                        let theories = state.repl.list_theories();
+                        if theories.is_empty() {
+                            state.log_info("No theories defined.");
+                        } else {
+                            state.log_info("Theories:");
+                            for t in theories {
+                                state.log_info(format!(
+                                    "  {} ({} sorts, {} rels, {} axioms)",
+                                    t.name, t.num_sorts, t.num_relations, t.num_axioms
+                                ));
+                            }
+                        }
+                    }
+                    ListTarget::Instances => {}
+                }
+                match target {
+                    ListTarget::Instances | ListTarget::All => {
+                        let instances = state.repl.list_instances();
+                        if instances.is_empty() {
+                            state.log_info("No instances defined.");
+                        } else {
+                            state.log_info("Instances:");
+                            for i in instances {
+                                state.log_info(format!(
+                                    "  {} : {} ({} elements)",
+                                    i.name, i.theory_name, i.num_elements
+                                ));
+                            }
+                        }
+                    }
+                    ListTarget::Theories => {}
+                }
+            }
+            MetaCommand::Inspect(name) => {
+                use crate::repl::{InspectResult, format_theory_detail, format_instance_detail};
+                match state.repl.inspect(&name) {
+                    Some(InspectResult::Theory(detail)) => {
+                        for line in format_theory_detail(&detail).lines() {
+                            state.log_info(line.to_string());
+                        }
+                    }
+                    Some(InspectResult::Instance(detail)) => {
+                        for line in format_instance_detail(&detail).lines() {
+                            state.log_info(line.to_string());
+                        }
+                    }
+                    None => {
+                        state.log_error(format!("Not found: {}", name));
+                    }
+                }
+            }
+            MetaCommand::Clear => {
+                state.clear_console();
+            }
+            MetaCommand::Reset => {
+                state.repl.reset();
+                state.selected_item = None;
+                state.log_success("State reset.");
+            }
+            MetaCommand::Chase { instance, max_iterations } => {
+                self.run_chase(state, &instance, max_iterations);
+            }
+            MetaCommand::Source(path) => {
+                match std::fs::read_to_string(&path) {
+                    Ok(content) => {
+                        state.editor_content = content;
+                        state.current_file = Some(path.clone());
+                        state.log_info(format!("Loaded: {}", path.display()));
+                        state.execute_editor();
+                    }
+                    Err(e) => {
+                        state.log_error(format!("Failed to load: {}", e));
+                    }
+                }
+            }
+            _ => {
+                state.log_warning("Command not yet implemented in GUI");
+            }
+        }
+    }
+
+    fn run_chase(&self, state: &mut GuiState, instance_name: &str, max_iterations: Option<usize>) {
+        use crate::core::RelationStorage;
+        use crate::query::chase::chase_fixpoint;
+
+        let theory_name = match state.repl.instances.get(instance_name) {
+            Some(e) => e.theory_name.clone(),
+            None => {
+                state.log_error(format!("Instance '{}' not found", instance_name));
+                return;
+            }
+        };
+
+        let theory = match state.repl.theories.get(&theory_name) {
+            Some(t) => t.clone(),
+            None => {
+                state.log_error(format!("Theory '{}' not found", theory_name));
+                return;
+            }
+        };
+
+        let sig = &theory.theory.signature;
+        let axioms = &theory.theory.axioms;
+
+        if axioms.is_empty() {
+            state.log_warning(format!("Theory '{}' has no axioms", theory_name));
+            return;
+        }
+
+        state.log_info(format!("Running chase on '{}' ({} axioms)...", instance_name, axioms.len()));
+
+        let entry = state.repl.instances.get_mut(instance_name).unwrap();
+        let max_iter = max_iterations.unwrap_or(100);
+
+        let start = std::time::Instant::now();
+        let result = chase_fixpoint(
+            axioms,
+            &mut entry.structure,
+            &mut state.repl.store.universe,
+            sig,
+            max_iter,
+        );
+
+        match result {
+            Ok(iterations) => {
+                let elapsed = start.elapsed();
+                // Capture structure info before releasing the borrow
+                let total_tuples: usize = entry.structure.relations.iter().map(|r| r.len()).sum();
+                let num_elements = entry.structure.len();
+
+                state.log_success(format!(
+                    "Chase completed in {} iterations ({:.2}ms)",
+                    iterations,
+                    elapsed.as_secs_f64() * 1000.0
+                ));
+                state.log_info(format!(
+                    "Structure: {} elements, {} relation tuples",
+                    num_elements,
+                    total_tuples
+                ));
+            }
+            Err(e) => {
+                state.log_error(format!("Chase error: {}", e));
+            }
+        }
+    }
+
+    fn history_up(&mut self) {
+        if self.history.is_empty() {
+            return;
+        }
+        match self.history_pos {
+            None => {
+                self.history_pos = Some(self.history.len() - 1);
+            }
+            Some(pos) if pos > 0 => {
+                self.history_pos = Some(pos - 1);
+            }
+            _ => {}
+        }
+        if let Some(pos) = self.history_pos {
+            self.input = self.history[pos].clone();
+        }
+    }
+
+    fn history_down(&mut self) {
+        match self.history_pos {
+            Some(pos) if pos + 1 < self.history.len() => {
+                self.history_pos = Some(pos + 1);
+                self.input = self.history[pos + 1].clone();
+            }
+            Some(_) => {
+                self.history_pos = None;
+                self.input.clear();
+            }
+            None => {}
+        }
+    }
+}
+
+impl Default for ConsolePanel {
+    fn default() -> Self {
+        Self::new()
+    }
+}

src/gui/panels/editor.rs

@@ -0,0 +1,216 @@
+//! Code editor panel
+//!
+//! Provides a multi-line text editor for writing Geolog code.
+
+use eframe::egui;
+
+use crate::gui::state::GuiState;
+
+/// Code editor panel
+pub struct EditorPanel {
+    /// Whether to show line numbers
+    show_line_numbers: bool,
+}
+
+impl EditorPanel {
+    pub fn new() -> Self {
+        Self {
+            show_line_numbers: true,
+        }
+    }
+
+    pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Header with title and buttons
+        ui.horizontal(|ui| {
+            ui.heading("Editor");
+
+            ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
+                if ui.button("Clear").clicked() {
+                    state.editor_content.clear();
+                }
+
+                if ui.button("Run").clicked() {
+                    state.execute_editor();
+                }
+
+                // Show current file if any
+                if let Some(path) = &state.current_file {
+                    ui.label(format!(
+                        "{}",
+                        path.file_name()
+                            .map(|s| s.to_string_lossy())
+                            .unwrap_or_default()
+                    ));
+                }
+            });
+        });
+
+        ui.separator();
+
+        // Editor area with syntax highlighting
+        egui::ScrollArea::vertical()
+            .auto_shrink([false, false])
+            .show(ui, |ui| {
+                self.show_editor_content(ui, state);
+            });
+    }
+
+    fn show_editor_content(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Use a monospace font for code
+        let font_id = egui::FontId::monospace(14.0);
+
+        // Calculate line numbers if needed
+        let line_count = state.editor_content.lines().count().max(1);
+        let line_number_width = if self.show_line_numbers {
+            let digits = (line_count as f32).log10().floor() as usize + 1;
+            digits.max(2) as f32 * 10.0 + 8.0
+        } else {
+            0.0
+        };
+
+        ui.horizontal(|ui| {
+            // Line numbers column
+            if self.show_line_numbers {
+                ui.allocate_ui_with_layout(
+                    egui::vec2(line_number_width, ui.available_height().max(0.0)),
+                    egui::Layout::top_down(egui::Align::RIGHT),
+                    |ui| {
+                        ui.style_mut().visuals.override_text_color =
+                            Some(egui::Color32::GRAY);
+
+                        for i in 1..=line_count {
+                            ui.label(
+                                egui::RichText::new(format!("{}", i))
+                                    .font(font_id.clone())
+                                    .color(egui::Color32::GRAY),
+                            );
+                        }
+                    },
+                );
+
+                ui.separator();
+            }
+
+            // Main editor area
+            let text_edit = egui::TextEdit::multiline(&mut state.editor_content)
+                .font(font_id)
+                .code_editor()
+                .desired_width(f32::INFINITY)
+                .desired_rows(20)
+                .lock_focus(true);
+
+            let response = ui.add(text_edit);
+
+            // Handle keyboard shortcuts
+            if response.has_focus() {
+                let modifiers = ui.input(|i| i.modifiers);
+                if modifiers.ctrl || modifiers.command {
+                    if ui.input(|i| i.key_pressed(egui::Key::Enter)) {
+                        state.execute_editor();
+                    }
+                }
+            }
+        });
+    }
+}
+
+impl Default for EditorPanel {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Simple syntax highlighting for Geolog code
+/// Returns a layouter function for egui's code_editor
+#[allow(dead_code)]
+fn geolog_highlighter(
+    _ui: &egui::Ui,
+    text: &str,
+    _wrap_width: f32,
+) -> egui::text::LayoutJob {
+    let mut job = egui::text::LayoutJob::default();
+
+    let keywords = [
+        "theory", "instance", "query", "forall", "exists", "Sort", "Prop", "true", "false",
+    ];
+
+    let font_id = egui::FontId::monospace(14.0);
+    let default_color = egui::Color32::WHITE;
+    let keyword_color = egui::Color32::from_rgb(86, 156, 214); // Blue
+    let comment_color = egui::Color32::from_rgb(106, 153, 85); // Green
+    let string_color = egui::Color32::from_rgb(206, 145, 120); // Orange
+
+    let mut chars = text.char_indices().peekable();
+
+    while let Some((i, c)) = chars.next() {
+        // Check for comments
+        if c == '/' && chars.peek().map(|(_, c)| *c) == Some('/') {
+            // Line comment - consume until end of line
+            let start = i;
+            while let Some((_, c)) = chars.next() {
+                if c == '\n' {
+                    break;
+                }
+            }
+            let end = chars.peek().map(|(i, _)| *i).unwrap_or(text.len());
+            job.append(
+                &text[start..end],
+                0.0,
+                egui::TextFormat::simple(font_id.clone(), comment_color),
+            );
+            continue;
+        }
+
+        // Check for strings
+        if c == '"' {
+            let start = i;
+            while let Some((_, c)) = chars.next() {
+                if c == '"' {
+                    break;
+                }
+                if c == '\\' {
+                    chars.next(); // Skip escaped character
+                }
+            }
+            let end = chars.peek().map(|(i, _)| *i).unwrap_or(text.len());
+            job.append(
+                &text[start..end],
+                0.0,
+                egui::TextFormat::simple(font_id.clone(), string_color),
+            );
+            continue;
+        }
+
+        // Check for identifiers/keywords
+        if c.is_alphabetic() || c == '_' {
+            let start = i;
+            while chars.peek().map(|(_, c)| c.is_alphanumeric() || *c == '_') == Some(true) {
+                chars.next();
+            }
+            let end = chars.peek().map(|(i, _)| *i).unwrap_or(text.len());
+            let word = &text[start..end];
+
+            let color = if keywords.contains(&word) {
+                keyword_color
+            } else {
+                default_color
+            };
+
+            job.append(
+                word,
+                0.0,
+                egui::TextFormat::simple(font_id.clone(), color),
+            );
+            continue;
+        }
+
+        // Default: single character
+        job.append(
+            &text[i..i + c.len_utf8()],
+            0.0,
+            egui::TextFormat::simple(font_id.clone(), default_color),
+        );
+    }
+
+    job
+}

src/gui/panels/inspector.rs

@@ -0,0 +1,318 @@
+//! Inspector panel for viewing theory/instance details
+//!
+//! Shows detailed information about the currently selected item.
+
+use eframe::egui;
+
+use crate::gui::state::{GuiState, SelectedItem};
+use crate::repl::{InstanceDetail, TheoryDetail};
+
+/// Inspector panel for viewing details
+pub struct InspectorPanel {}
+
+impl InspectorPanel {
+    pub fn new() -> Self {
+        Self {}
+    }
+
+    pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        ui.heading("Inspector");
+        ui.separator();
+
+        match &state.selected_item {
+            Some(SelectedItem::Theory(name)) => {
+                if let Some(detail) = state.selected_theory_detail() {
+                    self.show_theory_detail(ui, state, &detail);
+                } else {
+                    ui.label(format!("Theory '{}' not found", name));
+                }
+            }
+            Some(SelectedItem::Instance(name)) => {
+                if let Some(detail) = state.selected_instance_detail() {
+                    self.show_instance_detail(ui, state, &detail);
+                } else {
+                    ui.label(format!("Instance '{}' not found", name));
+                }
+            }
+            None => {
+                ui.label("Select a theory or instance to inspect");
+            }
+        }
+    }
+
+    fn show_theory_detail(&self, ui: &mut egui::Ui, state: &mut GuiState, detail: &TheoryDetail) {
+        // Theory header
+        ui.horizontal(|ui| {
+            ui.strong("Theory:");
+            ui.label(&detail.name);
+        });
+
+        // Parameters
+        if !detail.params.is_empty() {
+            ui.horizontal(|ui| {
+                ui.label("Parameters:");
+                for (name, theory) in &detail.params {
+                    ui.label(format!("{}: {}", name, theory));
+                }
+            });
+        }
+
+        ui.add_space(8.0);
+
+        egui::ScrollArea::vertical()
+            .auto_shrink([false, false])
+            .show(ui, |ui| {
+                // Sorts section
+                let sorts_response = egui::CollapsingHeader::new(format!("Sorts ({})", detail.sorts.len()))
+                    .default_open(state.inspector_sorts_expanded)
+                    .show(ui, |ui| {
+                        if detail.sorts.is_empty() {
+                            ui.label("(none)");
+                        } else {
+                            for sort in &detail.sorts {
+                                ui.label(format!("  {} : Sort", sort));
+                            }
+                        }
+                    });
+                state.inspector_sorts_expanded = sorts_response.fully_open();
+
+                // Functions section
+                let funcs_response = egui::CollapsingHeader::new(format!("Functions ({})", detail.functions.len()))
+                    .default_open(state.inspector_functions_expanded)
+                    .show(ui, |ui| {
+                        if detail.functions.is_empty() {
+                            ui.label("(none)");
+                        } else {
+                            for (name, domain, codomain) in &detail.functions {
+                                ui.label(format!("  {} : {} -> {}", name, domain, codomain));
+                            }
+                        }
+                    });
+                state.inspector_functions_expanded = funcs_response.fully_open();
+
+                // Relations section
+                let rels_response = egui::CollapsingHeader::new(format!("Relations ({})", detail.relations.len()))
+                    .default_open(state.inspector_relations_expanded)
+                    .show(ui, |ui| {
+                        if detail.relations.is_empty() {
+                            ui.label("(none)");
+                        } else {
+                            for (name, domain) in &detail.relations {
+                                ui.label(format!("  {} : {} -> Prop", name, domain));
+                            }
+                        }
+                    });
+                state.inspector_relations_expanded = rels_response.fully_open();
+
+                // Instance fields section
+                if !detail.instance_fields.is_empty() {
+                    egui::CollapsingHeader::new(format!(
+                        "Instance Fields ({})",
+                        detail.instance_fields.len()
+                    ))
+                    .default_open(true)
+                    .show(ui, |ui| {
+                        for (name, theory_type) in &detail.instance_fields {
+                            ui.label(format!("  {} : {} instance", name, theory_type));
+                        }
+                    });
+                }
+
+                // Axioms section
+                let axioms_response = egui::CollapsingHeader::new(format!("Axioms ({})", detail.axioms.len()))
+                    .default_open(state.inspector_axioms_expanded)
+                    .show(ui, |ui| {
+                        if detail.axioms.is_empty() {
+                            ui.label("(none)");
+                        } else {
+                            for (i, axiom) in detail.axioms.iter().enumerate() {
+                                let context_str: Vec<String> = axiom
+                                    .context
+                                    .iter()
+                                    .map(|(name, sort)| format!("{}: {}", name, sort))
+                                    .collect();
+
+                                let axiom_str = if axiom.premise == "true" {
+                                    format!(
+                                        "[{}] forall {}. |- {}",
+                                        i,
+                                        context_str.join(", "),
+                                        axiom.conclusion
+                                    )
+                                } else {
+                                    format!(
+                                        "[{}] forall {}. {} |- {}",
+                                        i,
+                                        context_str.join(", "),
+                                        axiom.premise,
+                                        axiom.conclusion
+                                    )
+                                };
+                                ui.label(axiom_str);
+                            }
+                        }
+                    });
+                state.inspector_axioms_expanded = axioms_response.fully_open();
+            });
+    }
+
+    fn show_instance_detail(
+        &self,
+        ui: &mut egui::Ui,
+        state: &mut GuiState,
+        detail: &InstanceDetail,
+    ) {
+        // Instance header
+        ui.horizontal(|ui| {
+            ui.strong("Instance:");
+            ui.label(&detail.name);
+            ui.label(":");
+            ui.label(&detail.theory_name);
+        });
+
+        ui.add_space(8.0);
+
+        // Action buttons
+        ui.horizontal(|ui| {
+            let detail_name = detail.name.clone();
+            if ui.button("View Graph").clicked() {
+                state.show_graph(&detail_name, None);
+            }
+            if ui.button("Run Chase").clicked() {
+                state.log_info(format!("Use Chase menu to run chase on '{}'", detail_name));
+            }
+        });
+
+        ui.add_space(8.0);
+
+        egui::ScrollArea::vertical()
+            .auto_shrink([false, false])
+            .show(ui, |ui| {
+                // Elements section
+                let total_elements: usize = detail.elements.iter().map(|(_, v)| v.len()).sum();
+                let elems_response = egui::CollapsingHeader::new(format!("Elements ({})", total_elements))
+                    .default_open(state.inspector_elements_expanded)
+                    .show(ui, |ui| {
+                        if detail.elements.is_empty() {
+                            ui.label("(none)");
+                        } else {
+                            for (sort_name, elements) in &detail.elements {
+                                ui.horizontal(|ui| {
+                                    ui.strong(format!("{} ({}):", sort_name, elements.len()));
+                                });
+                                ui.indent("elements", |ui| {
+                                    // Show elements in a grid if there are many
+                                    if elements.len() <= 10 {
+                                        for elem in elements {
+                                            ui.label(format!("  {}", elem));
+                                        }
+                                    } else {
+                                        // Show first few and a count
+                                        for elem in elements.iter().take(5) {
+                                            ui.label(format!("  {}", elem));
+                                        }
+                                        ui.label(format!("  ... and {} more", elements.len() - 5));
+                                    }
+                                });
+                            }
+                        }
+                    });
+                state.inspector_elements_expanded = elems_response.fully_open();
+
+                // Functions section
+                let total_func_values: usize = detail.functions.iter().map(|(_, v)| v.len()).sum();
+                if total_func_values > 0 {
+                    egui::CollapsingHeader::new(format!("Function Values ({})", total_func_values))
+                        .default_open(state.inspector_functions_expanded)
+                        .show(ui, |ui| {
+                            for (func_name, values) in &detail.functions {
+                                ui.horizontal(|ui| {
+                                    ui.strong(format!("{} ({}):", func_name, values.len()));
+                                });
+                                ui.indent("func_values", |ui| {
+                                    if values.len() <= 10 {
+                                        for value in values {
+                                            ui.label(format!("  {}", value));
+                                        }
+                                    } else {
+                                        for value in values.iter().take(5) {
+                                            ui.label(format!("  {}", value));
+                                        }
+                                        ui.label(format!("  ... and {} more", values.len() - 5));
+                                    }
+                                });
+                            }
+                        });
+                }
+
+                // Relations section
+                let total_tuples: usize = detail.relations.iter().map(|(_, _, t)| t.len()).sum();
+                if total_tuples > 0 {
+                    egui::CollapsingHeader::new(format!("Relations ({} tuples)", total_tuples))
+                        .default_open(state.inspector_relations_expanded)
+                        .show(ui, |ui| {
+                            for (rel_name, field_names, tuples) in &detail.relations {
+                                ui.horizontal(|ui| {
+                                    ui.strong(format!("{} ({} tuples):", rel_name, tuples.len()));
+
+                                    // Add button to view as graph
+                                    let detail_name = detail.name.clone();
+                                    let rel_name_clone = rel_name.clone();
+                                    if ui.small_button("View Graph").clicked() {
+                                        state.show_graph(&detail_name, Some(&rel_name_clone));
+                                    }
+                                });
+
+                                ui.indent("rel_tuples", |ui| {
+                                    let display_tuples = if tuples.len() <= 10 {
+                                        tuples.as_slice()
+                                    } else {
+                                        &tuples[..5]
+                                    };
+
+                                    for tuple in display_tuples {
+                                        let tuple_str = if field_names.is_empty() {
+                                            // Unary relation
+                                            format!("  {} {}", tuple.join(", "), rel_name)
+                                        } else {
+                                            // Multi-ary relation with field names
+                                            let fields: Vec<String> = field_names
+                                                .iter()
+                                                .zip(tuple.iter())
+                                                .map(|(f, v)| format!("{}: {}", f, v))
+                                                .collect();
+                                            format!("  [{}] {}", fields.join(", "), rel_name)
+                                        };
+                                        ui.label(tuple_str);
+                                    }
+
+                                    if tuples.len() > 10 {
+                                        ui.label(format!("  ... and {} more", tuples.len() - 5));
+                                    }
+                                });
+                            }
+                        });
+                }
+
+                // Nested instances section
+                if !detail.nested.is_empty() {
+                    egui::CollapsingHeader::new(format!(
+                        "Nested Instances ({})",
+                        detail.nested.len()
+                    ))
+                    .default_open(true)
+                    .show(ui, |ui| {
+                        for (field_name, elem_count) in &detail.nested {
+                            ui.label(format!("  {} ({} elements)", field_name, elem_count));
+                        }
+                    });
+                }
+            });
+    }
+}
+
+impl Default for InspectorPanel {
+    fn default() -> Self {
+        Self::new()
+    }
+}

src/gui/panels/mod.rs

@@ -0,0 +1,11 @@
+//! GUI panels for the Geolog application
+
+pub mod browser;
+pub mod console;
+pub mod editor;
+pub mod inspector;
+
+pub use browser::BrowserPanel;
+pub use console::ConsolePanel;
+pub use editor::EditorPanel;
+pub use inspector::InspectorPanel;

src/gui/state.rs

@@ -0,0 +1,321 @@
+//! GUI state management
+//!
+//! Wraps ReplState with GUI-specific state for the egui application.
+
+use std::collections::HashSet;
+use std::path::PathBuf;
+
+use crate::repl::{InstanceDetail, ReplState, TheoryDetail};
+
+/// What item is currently selected in the browser
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum SelectedItem {
+    Theory(String),
+    Instance(String),
+}
+
+/// A message displayed in the console
+#[derive(Clone, Debug)]
+pub struct ConsoleMessage {
+    pub text: String,
+    pub kind: MessageKind,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum MessageKind {
+    Info,
+    Success,
+    Error,
+    Warning,
+}
+
+/// A recorded chase event for visualization
+#[derive(Clone, Debug)]
+pub struct ChaseEventRecord {
+    pub iteration: usize,
+    pub axiom_index: usize,
+    pub axiom_name: Option<String>,
+    pub binding: Vec<(String, String)>, // (var_name, element_name)
+    pub changed: bool,
+}
+
+/// Chase execution mode
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum ChaseMode {
+    /// Not running
+    Idle,
+    /// Stepping through events
+    Stepping,
+    /// Running continuously
+    Running,
+    /// Chase completed
+    Completed,
+}
+
+/// State for chase visualization
+#[derive(Clone, Debug)]
+pub struct ChaseVisualizationState {
+    pub mode: ChaseMode,
+    pub instance_name: String,
+    pub events: Vec<ChaseEventRecord>,
+    pub current_event: usize,
+    pub current_iteration: usize,
+    pub breakpoints: HashSet<String>,
+    pub total_iterations: Option<usize>,
+}
+
+impl ChaseVisualizationState {
+    pub fn new(instance_name: String) -> Self {
+        Self {
+            mode: ChaseMode::Idle,
+            instance_name,
+            events: Vec::new(),
+            current_event: 0,
+            current_iteration: 0,
+            breakpoints: HashSet::new(),
+            total_iterations: None,
+        }
+    }
+
+    pub fn record_event(&mut self, event: ChaseEventRecord) {
+        self.events.push(event);
+    }
+
+    pub fn step(&mut self) {
+        if self.current_event < self.events.len().saturating_sub(1) {
+            self.current_event += 1;
+        }
+    }
+
+    pub fn has_next(&self) -> bool {
+        self.current_event < self.events.len().saturating_sub(1)
+    }
+}
+
+/// Central view mode
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Default)]
+pub enum CentralView {
+    #[default]
+    EditorAndInspector,
+    ChaseVisualization,
+    GraphVisualization,
+}
+
+/// GUI state wrapping ReplState
+pub struct GuiState {
+    /// The underlying REPL state (theories, instances, store)
+    pub repl: ReplState,
+
+    /// Currently selected item in the browser
+    pub selected_item: Option<SelectedItem>,
+
+    /// Content of the code editor
+    pub editor_content: String,
+
+    /// Console output messages
+    pub console_messages: Vec<ConsoleMessage>,
+
+    /// Chase visualization state (if running)
+    pub chase_state: Option<ChaseVisualizationState>,
+
+    /// Graph view state
+    pub graph_instance: Option<String>,
+    pub graph_relation: Option<String>,
+
+    /// Currently loaded file path (if any)
+    pub current_file: Option<PathBuf>,
+
+    /// Current view mode for the central panel
+    pub central_view: CentralView,
+
+    /// Whether the browser tree sections are expanded
+    pub theories_expanded: bool,
+    pub instances_expanded: bool,
+
+    /// Inspector collapsible sections
+    pub inspector_sorts_expanded: bool,
+    pub inspector_functions_expanded: bool,
+    pub inspector_relations_expanded: bool,
+    pub inspector_axioms_expanded: bool,
+    pub inspector_elements_expanded: bool,
+}
+
+impl Default for GuiState {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+impl GuiState {
+    pub fn new() -> Self {
+        Self {
+            repl: ReplState::new(),
+            selected_item: None,
+            editor_content: String::new(),
+            console_messages: Vec::new(),
+            chase_state: None,
+            graph_instance: None,
+            graph_relation: None,
+            current_file: None,
+            central_view: CentralView::EditorAndInspector,
+            theories_expanded: true,
+            instances_expanded: true,
+            inspector_sorts_expanded: true,
+            inspector_functions_expanded: true,
+            inspector_relations_expanded: true,
+            inspector_axioms_expanded: true,
+            inspector_elements_expanded: true,
+        }
+    }
+
+    /// Create a new GUI state with a workspace path for persistence
+    pub fn with_path(path: impl Into<PathBuf>) -> Self {
+        Self {
+            repl: ReplState::with_path(path),
+            ..Self::new()
+        }
+    }
+
+    /// Add an info message to the console
+    pub fn log_info(&mut self, text: impl Into<String>) {
+        self.console_messages.push(ConsoleMessage {
+            text: text.into(),
+            kind: MessageKind::Info,
+        });
+    }
+
+    /// Add a success message to the console
+    pub fn log_success(&mut self, text: impl Into<String>) {
+        self.console_messages.push(ConsoleMessage {
+            text: text.into(),
+            kind: MessageKind::Success,
+        });
+    }
+
+    /// Add an error message to the console
+    pub fn log_error(&mut self, text: impl Into<String>) {
+        self.console_messages.push(ConsoleMessage {
+            text: text.into(),
+            kind: MessageKind::Error,
+        });
+    }
+
+    /// Add a warning message to the console
+    pub fn log_warning(&mut self, text: impl Into<String>) {
+        self.console_messages.push(ConsoleMessage {
+            text: text.into(),
+            kind: MessageKind::Warning,
+        });
+    }
+
+    /// Clear all console messages
+    pub fn clear_console(&mut self) {
+        self.console_messages.clear();
+    }
+
+    /// Execute the editor content as geolog code
+    pub fn execute_editor(&mut self) {
+        let source = self.editor_content.clone();
+        if source.trim().is_empty() {
+            return;
+        }
+
+        match self.repl.execute_geolog(&source) {
+            Ok(results) => {
+                for result in results {
+                    match result {
+                        crate::repl::ExecuteResult::Namespace(name) => {
+                            self.log_info(format!("Namespace: {}", name));
+                        }
+                        crate::repl::ExecuteResult::Theory {
+                            name,
+                            num_sorts,
+                            num_functions,
+                            num_relations,
+                            num_axioms,
+                        } => {
+                            let mut parts = vec![format!("{} sorts", num_sorts)];
+                            if num_functions > 0 {
+                                parts.push(format!("{} functions", num_functions));
+                            }
+                            if num_relations > 0 {
+                                parts.push(format!("{} relations", num_relations));
+                            }
+                            if num_axioms > 0 {
+                                parts.push(format!("{} axioms", num_axioms));
+                            }
+                            self.log_success(format!(
+                                "Defined theory {} ({})",
+                                name,
+                                parts.join(", ")
+                            ));
+                        }
+                        crate::repl::ExecuteResult::Instance {
+                            name,
+                            theory_name,
+                            num_elements,
+                        } => {
+                            self.log_success(format!(
+                                "Defined instance {} : {} ({} elements)",
+                                name, theory_name, num_elements
+                            ));
+                        }
+                        crate::repl::ExecuteResult::Query(_result) => {
+                            self.log_info("Query executed");
+                        }
+                    }
+                }
+            }
+            Err(e) => {
+                self.log_error(format!("Error: {}", e));
+            }
+        }
+    }
+
+    /// Load a file into the editor
+    pub fn load_file(&mut self, path: &PathBuf) {
+        match std::fs::read_to_string(path) {
+            Ok(content) => {
+                self.editor_content = content;
+                self.current_file = Some(path.clone());
+                self.log_info(format!("Loaded: {}", path.display()));
+            }
+            Err(e) => {
+                self.log_error(format!("Failed to load {}: {}", path.display(), e));
+            }
+        }
+    }
+
+    /// Get the currently selected theory detail
+    pub fn selected_theory_detail(&self) -> Option<TheoryDetail> {
+        if let Some(SelectedItem::Theory(name)) = &self.selected_item {
+            if let Some(crate::repl::InspectResult::Theory(detail)) = self.repl.inspect(name) {
+                return Some(detail);
+            }
+        }
+        None
+    }
+
+    /// Get the currently selected instance detail
+    pub fn selected_instance_detail(&self) -> Option<InstanceDetail> {
+        if let Some(SelectedItem::Instance(name)) = &self.selected_item {
+            if let Some(crate::repl::InspectResult::Instance(detail)) = self.repl.inspect(name) {
+                return Some(detail);
+            }
+        }
+        None
+    }
+
+    /// Start a chase visualization for an instance
+    pub fn start_chase(&mut self, instance_name: &str) {
+        self.chase_state = Some(ChaseVisualizationState::new(instance_name.to_string()));
+        self.central_view = CentralView::ChaseVisualization;
+    }
+
+    /// Start graph visualization for an instance and relation
+    pub fn show_graph(&mut self, instance_name: &str, relation_name: Option<&str>) {
+        self.graph_instance = Some(instance_name.to_string());
+        self.graph_relation = relation_name.map(|s| s.to_string());
+        self.central_view = CentralView::GraphVisualization;
+    }
+}

src/gui/visualizations/chase.rs

@@ -0,0 +1,497 @@
+//! Chase algorithm visualization
+//!
+//! Provides step-through debugging and visualization of the chase algorithm.
+
+use eframe::egui;
+
+use crate::core::RelationStorage;
+use crate::gui::state::{ChaseEventRecord, ChaseMode, ChaseVisualizationState, CentralView, GuiState, SelectedItem};
+use crate::query::chase::{ChaseControl, ChaseEvent, ChaseObserver};
+
+/// Chase visualization panel
+pub struct ChaseVisualization {
+    /// Breakpoint being added
+    new_breakpoint: String,
+}
+
+impl ChaseVisualization {
+    pub fn new() -> Self {
+        Self {
+            new_breakpoint: String::new(),
+        }
+    }
+
+    pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Header
+        ui.horizontal(|ui| {
+            ui.heading("Chase Visualization");
+
+            if let Some(chase_state) = &state.chase_state {
+                ui.label(format!("Instance: {}", chase_state.instance_name));
+            }
+        });
+
+        ui.separator();
+
+        if state.chase_state.is_none() {
+            self.show_start_panel(ui, state);
+        } else {
+            self.show_chase_panel(ui, state);
+        }
+    }
+
+    fn show_start_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        ui.label("Select an instance to start chase visualization:");
+        ui.add_space(8.0);
+
+        let instances = state.repl.list_instances();
+        if instances.is_empty() {
+            ui.label("No instances defined. Create an instance first.");
+        } else {
+            for instance in instances {
+                if ui.button(format!("{} : {}", instance.name, instance.theory_name)).clicked() {
+                    state.start_chase(&instance.name);
+                }
+            }
+        }
+
+        // Or use currently selected instance
+        if let Some(SelectedItem::Instance(name)) = &state.selected_item {
+            ui.add_space(16.0);
+            let name = name.clone();
+            if ui.button(format!("Start Chase on selected: {}", name)).clicked() {
+                state.start_chase(&name);
+            }
+        }
+    }
+
+    fn show_chase_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Read mode and instance_name before mutable operations
+        let (mode, instance_name) = {
+            let chase_state = state.chase_state.as_ref().unwrap();
+            (chase_state.mode, chase_state.instance_name.clone())
+        };
+
+        // Control buttons
+        let mut step_clicked = false;
+        let mut run_clicked = false;
+        let mut stop_clicked = false;
+        let mut reset_clicked = false;
+        let mut close_clicked = false;
+
+        ui.horizontal(|ui| {
+            // Mode indicator
+            let mode_text = match mode {
+                ChaseMode::Idle => "Idle",
+                ChaseMode::Stepping => "Stepping",
+                ChaseMode::Running => "Running",
+                ChaseMode::Completed => "Completed",
+            };
+            ui.label(format!("Mode: {}", mode_text));
+
+            ui.separator();
+
+            // Only show Run/Step if not completed
+            if mode != ChaseMode::Completed {
+                if ui.button("Step").clicked() {
+                    step_clicked = true;
+                }
+
+                if ui.button("Run All").clicked() {
+                    run_clicked = true;
+                }
+
+                if ui.button("Stop").clicked() {
+                    stop_clicked = true;
+                }
+            }
+
+            // Reset button
+            if ui.button("Reset").clicked() {
+                reset_clicked = true;
+            }
+
+            // Close button
+            if ui.button("Close").clicked() {
+                close_clicked = true;
+            }
+        });
+
+        // Handle button actions
+        if step_clicked {
+            self.step_chase(state);
+        }
+        if run_clicked {
+            self.run_chase_to_completion(state);
+        }
+        if stop_clicked {
+            if let Some(chase_state) = &mut state.chase_state {
+                chase_state.mode = ChaseMode::Completed;
+            }
+        }
+        if reset_clicked {
+            state.chase_state = Some(ChaseVisualizationState::new(instance_name));
+        }
+        if close_clicked {
+            state.chase_state = None;
+            state.central_view = CentralView::EditorAndInspector;
+            return;
+        }
+
+        ui.separator();
+
+        // Main content area split into events and info
+        ui.columns(2, |columns| {
+            // Left column: Events
+            columns[0].heading("Events");
+            self.show_events_panel(&mut columns[0], state);
+
+            // Right column: Info and breakpoints
+            columns[1].heading("Information");
+            self.show_info_panel(&mut columns[1], state);
+        });
+    }
+
+    fn show_events_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        egui::ScrollArea::vertical()
+            .auto_shrink([false, false])
+            .stick_to_bottom(true)
+            .show(ui, |ui| {
+                if let Some(chase_state) = &state.chase_state {
+                    if chase_state.events.is_empty() {
+                        ui.label("No events yet. Click 'Step' or 'Run All' to start.");
+                    } else {
+                        for (i, event) in chase_state.events.iter().enumerate() {
+                            let is_current = i == chase_state.current_event;
+                            let prefix = if is_current { ">" } else { " " };
+
+                            let axiom_name = event.axiom_name.as_deref().unwrap_or("(unnamed)");
+                            let binding_str: Vec<String> = event
+                                .binding
+                                .iter()
+                                .map(|(var, val)| format!("{}={}", var, val))
+                                .collect();
+
+                            let changed_marker = if event.changed { " [changed]" } else { "" };
+
+                            let text = format!(
+                                "{} [{}] #{} {} {{ {} }}{}",
+                                prefix,
+                                event.iteration,
+                                event.axiom_index,
+                                axiom_name,
+                                binding_str.join(", "),
+                                changed_marker
+                            );
+
+                            let color = if is_current {
+                                egui::Color32::YELLOW
+                            } else if event.changed {
+                                egui::Color32::from_rgb(100, 200, 100)
+                            } else {
+                                egui::Color32::LIGHT_GRAY
+                            };
+
+                            ui.label(egui::RichText::new(text).color(color).monospace());
+                        }
+                    }
+                }
+            });
+    }
+
+    fn show_info_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Read info from chase_state
+        let (current_iteration, total_iterations, events_count, breakpoints, instance_name) = {
+            if let Some(chase_state) = &state.chase_state {
+                (
+                    chase_state.current_iteration,
+                    chase_state.total_iterations,
+                    chase_state.events.len(),
+                    chase_state.breakpoints.iter().cloned().collect::<Vec<_>>(),
+                    chase_state.instance_name.clone(),
+                )
+            } else {
+                return;
+            }
+        };
+
+        // Iteration info
+        ui.label(format!("Current iteration: {}", current_iteration));
+        if let Some(total) = total_iterations {
+            ui.label(format!("Total iterations: {}", total));
+        }
+        ui.label(format!("Events recorded: {}", events_count));
+
+        ui.add_space(16.0);
+
+        // Breakpoints section
+        ui.heading("Breakpoints");
+
+        // Add new breakpoint
+        ui.horizontal(|ui| {
+            ui.text_edit_singleline(&mut self.new_breakpoint);
+            if ui.button("+").clicked() && !self.new_breakpoint.is_empty() {
+                if let Some(chase_state) = &mut state.chase_state {
+                    chase_state.breakpoints.insert(self.new_breakpoint.clone());
+                }
+                self.new_breakpoint.clear();
+            }
+        });
+
+        // List breakpoints
+        if breakpoints.is_empty() {
+            ui.label("(no breakpoints)");
+        } else {
+            let mut to_remove = None;
+            for bp in &breakpoints {
+                ui.horizontal(|ui| {
+                    ui.label(format!("  {}", bp));
+                    if ui.small_button("x").clicked() {
+                        to_remove = Some(bp.clone());
+                    }
+                });
+            }
+            if let Some(bp) = to_remove {
+                if let Some(chase_state) = &mut state.chase_state {
+                    chase_state.breakpoints.remove(&bp);
+                }
+            }
+        }
+
+        ui.add_space(16.0);
+
+        // Structure info
+        ui.heading("Structure");
+        if let Some(entry) = state.repl.instances.get(&instance_name) {
+            ui.label(format!("Elements: {}", entry.structure.len()));
+
+            let total_tuples: usize = entry.structure.relations.iter().map(|r| r.len()).sum();
+            ui.label(format!("Relation tuples: {}", total_tuples));
+
+            // Show relation breakdown
+            let theory_name = entry.theory_name.clone();
+            if let Some(theory) = state.repl.theories.get(&theory_name) {
+                for (rel_id, rel) in theory.theory.signature.relations.iter().enumerate() {
+                    if rel_id < entry.structure.relations.len() {
+                        let count = entry.structure.relations[rel_id].len();
+                        if count > 0 {
+                            ui.label(format!("  {}: {} tuples", rel.name, count));
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    /// Execute a single step of the chase
+    fn step_chase(&mut self, state: &mut GuiState) {
+        let instance_name = match &state.chase_state {
+            Some(s) => s.instance_name.clone(),
+            None => return,
+        };
+
+        let current_iteration = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0);
+
+        // Get theory name first (immutable borrow)
+        let theory_name = match state.repl.instances.get(&instance_name) {
+            Some(e) => e.theory_name.clone(),
+            None => {
+                state.log_error(format!("Instance '{}' not found", instance_name));
+                return;
+            }
+        };
+
+        let theory = match state.repl.theories.get(&theory_name) {
+            Some(t) => t.clone(),
+            None => {
+                state.log_error(format!("Theory '{}' not found", theory_name));
+                return;
+            }
+        };
+
+        // Now get mutable access to entry
+        let entry = state.repl.instances.get_mut(&instance_name).unwrap();
+
+        // Create a GUI observer that records events
+        let mut observer = GuiChaseObserver {
+            events: Vec::new(),
+            slid_to_name: &entry.slid_to_name,
+            iteration: current_iteration,
+            step_mode: true,
+            steps_remaining: 1,
+        };
+
+        // Run chase with observer (just one step)
+        let sig = &theory.theory.signature;
+        let axioms = &theory.theory.axioms;
+        let axiom_names = &theory.theory.axiom_names;
+
+        let result = crate::query::chase::chase_fixpoint_with_observer(
+            axioms,
+            axiom_names,
+            &mut entry.structure,
+            &mut state.repl.store.universe,
+            sig,
+            1, // Just one iteration
+            &mut observer,
+        );
+
+        // Record events
+        let events = observer.events;
+        if let Some(chase_state) = &mut state.chase_state {
+            chase_state.mode = ChaseMode::Stepping;
+            for event in events {
+                chase_state.events.push(event);
+            }
+            chase_state.current_event = chase_state.events.len().saturating_sub(1);
+            chase_state.current_iteration += 1;
+
+            if let Ok(iterations) = result {
+                if iterations == 0 {
+                    chase_state.mode = ChaseMode::Completed;
+                    chase_state.total_iterations = Some(chase_state.current_iteration);
+                }
+            }
+        }
+
+        // Log completion separately
+        if let Ok(iterations) = result {
+            if iterations == 0 {
+                let total = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0);
+                state.log_success(format!("Chase completed after {} iterations", total));
+            }
+        }
+    }
+
+    /// Run the chase to completion
+    fn run_chase_to_completion(&mut self, state: &mut GuiState) {
+        let instance_name = match &state.chase_state {
+            Some(s) => s.instance_name.clone(),
+            None => return,
+        };
+
+        // Get theory name first (immutable borrow)
+        let theory_name = match state.repl.instances.get(&instance_name) {
+            Some(e) => e.theory_name.clone(),
+            None => {
+                state.log_error(format!("Instance '{}' not found", instance_name));
+                return;
+            }
+        };
+
+        let theory = match state.repl.theories.get(&theory_name) {
+            Some(t) => t.clone(),
+            None => {
+                state.log_error(format!("Theory '{}' not found", theory_name));
+                return;
+            }
+        };
+
+        // Now get mutable access to entry
+        let entry = state.repl.instances.get_mut(&instance_name).unwrap();
+
+        // Run chase to fixpoint
+        let sig = &theory.theory.signature;
+        let axioms = &theory.theory.axioms;
+
+        let start = std::time::Instant::now();
+        let result = crate::query::chase::chase_fixpoint(
+            axioms,
+            &mut entry.structure,
+            &mut state.repl.store.universe,
+            sig,
+            100,
+        );
+
+        match result {
+            Ok(iterations) => {
+                let elapsed = start.elapsed();
+                if let Some(chase_state) = &mut state.chase_state {
+                    chase_state.mode = ChaseMode::Completed;
+                    chase_state.total_iterations = Some(iterations);
+                }
+                state.log_success(format!(
+                    "Chase completed in {} iterations ({:.2}ms)",
+                    iterations,
+                    elapsed.as_secs_f64() * 1000.0
+                ));
+            }
+            Err(e) => {
+                state.log_error(format!("Chase error: {}", e));
+            }
+        }
+    }
+}
+
+impl Default for ChaseVisualization {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Observer that records chase events for the GUI
+struct GuiChaseObserver<'a> {
+    events: Vec<ChaseEventRecord>,
+    slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>,
+    iteration: usize,
+    step_mode: bool,
+    steps_remaining: usize,
+}
+
+impl<'a> ChaseObserver for GuiChaseObserver<'a> {
+    fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl {
+        match event {
+            ChaseEvent::IterationStart { iteration } => {
+                self.iteration = iteration;
+                ChaseControl::Continue
+            }
+            ChaseEvent::AxiomFiring {
+                axiom_index,
+                axiom_name,
+                binding,
+                violation_count: _,
+            } => {
+                // Record the event
+                let binding_vec: Vec<(String, String)> = binding
+                    .iter()
+                    .map(|(var, slid)| {
+                        let elem_name = self
+                            .slid_to_name
+                            .get(slid)
+                            .cloned()
+                            .unwrap_or_else(|| format!("#{}", slid));
+                        (var.clone(), elem_name)
+                    })
+                    .collect();
+
+                self.events.push(ChaseEventRecord {
+                    iteration: self.iteration,
+                    axiom_index,
+                    axiom_name: axiom_name.map(|s| s.to_string()),
+                    binding: binding_vec,
+                    changed: false, // Will be updated in AxiomFired
+                });
+
+                if self.step_mode {
+                    self.steps_remaining = self.steps_remaining.saturating_sub(1);
+                    if self.steps_remaining == 0 {
+                        ChaseControl::Stop
+                    } else {
+                        ChaseControl::Continue
+                    }
+                } else {
+                    ChaseControl::Continue
+                }
+            }
+            ChaseEvent::AxiomFired { changed, .. } => {
+                // Update the last event with the changed status
+                if let Some(last) = self.events.last_mut() {
+                    last.changed = changed;
+                }
+                ChaseControl::Continue
+            }
+            ChaseEvent::IterationEnd { .. } => ChaseControl::Continue,
+            ChaseEvent::ChaseComplete { .. } => ChaseControl::Continue,
+        }
+    }
+}

src/gui/visualizations/graph.rs

@@ -0,0 +1,566 @@
+//! Relation graph visualization
+//!
+//! Displays elements as nodes and relation tuples as edges.
+
+use eframe::egui;
+use std::collections::HashMap;
+
+use crate::core::RelationStorage;
+use crate::gui::state::{CentralView, GuiState};
+use crate::id::{NumericId, Slid};
+
+/// A node in the graph
+#[derive(Clone, Debug)]
+pub struct GraphNode {
+    pub id: Slid,
+    pub name: String,
+    pub sort: String,
+    pub position: egui::Pos2,
+    pub color: egui::Color32,
+}
+
+/// An edge in the graph
+#[derive(Clone, Debug)]
+pub struct GraphEdge {
+    pub from: Slid,
+    pub to: Slid,
+    pub relation: String,
+    pub label: Option<String>,
+}
+
+/// Graph view panel
+pub struct GraphView {
+    /// Nodes in the graph
+    nodes: Vec<GraphNode>,
+    /// Edges in the graph
+    edges: Vec<GraphEdge>,
+    /// Node positions (for dragging)
+    node_positions: HashMap<Slid, egui::Pos2>,
+    /// Currently dragged node
+    dragged_node: Option<Slid>,
+    /// Zoom level
+    zoom: f32,
+    /// Pan offset
+    pan: egui::Vec2,
+    /// Selected relation filter
+    selected_relation: Option<String>,
+    /// Whether we need to recalculate layout
+    needs_layout: bool,
+    /// Last instance/relation we rendered
+    last_instance: Option<String>,
+    last_relation: Option<String>,
+}
+
+impl GraphView {
+    pub fn new() -> Self {
+        Self {
+            nodes: Vec::new(),
+            edges: Vec::new(),
+            node_positions: HashMap::new(),
+            dragged_node: None,
+            zoom: 1.0,
+            pan: egui::Vec2::ZERO,
+            selected_relation: None,
+            needs_layout: true,
+            last_instance: None,
+            last_relation: None,
+        }
+    }
+
+    pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        // Header
+        ui.horizontal(|ui| {
+            ui.heading("Graph Visualization");
+
+            if let Some(instance) = &state.graph_instance {
+                ui.label(format!("Instance: {}", instance));
+            }
+            if let Some(relation) = &state.graph_relation {
+                ui.label(format!("Relation: {}", relation));
+            }
+        });
+
+        ui.separator();
+
+        // Check if we need to rebuild the graph
+        if state.graph_instance != self.last_instance || state.graph_relation != self.last_relation {
+            self.rebuild_graph(state);
+        }
+
+        // No instance selected
+        if state.graph_instance.is_none() {
+            self.show_selection_panel(ui, state);
+            return;
+        }
+
+        // Controls
+        ui.horizontal(|ui| {
+            // Relation filter dropdown
+            if let Some(instance_name) = &state.graph_instance {
+                if let Some(entry) = state.repl.instances.get(instance_name) {
+                    if let Some(theory) = state.repl.theories.get(&entry.theory_name) {
+                        let relations: Vec<&str> = theory
+                            .theory
+                            .signature
+                            .relations
+                            .iter()
+                            .map(|r| r.name.as_str())
+                            .collect();
+
+                        ui.label("Relation:");
+                        egui::ComboBox::from_label("")
+                            .selected_text(
+                                self.selected_relation
+                                    .as_deref()
+                                    .unwrap_or("(all)"),
+                            )
+                            .show_ui(ui, |ui| {
+                                if ui.selectable_label(self.selected_relation.is_none(), "(all)").clicked() {
+                                    self.selected_relation = None;
+                                    self.needs_layout = true;
+                                }
+                                for rel in relations {
+                                    if ui.selectable_label(
+                                        self.selected_relation.as_deref() == Some(rel),
+                                        rel,
+                                    ).clicked() {
+                                        self.selected_relation = Some(rel.to_string());
+                                        self.needs_layout = true;
+                                    }
+                                }
+                            });
+                    }
+                }
+            }
+
+            ui.separator();
+
+            if ui.button("Reset Layout").clicked() {
+                self.needs_layout = true;
+            }
+
+            if ui.button("Fit").clicked() {
+                self.fit_to_view(ui);
+            }
+
+            // Zoom controls
+            ui.label("Zoom:");
+            if ui.button("-").clicked() {
+                self.zoom = (self.zoom - 0.1).max(0.1);
+            }
+            ui.label(format!("{:.0}%", self.zoom * 100.0));
+            if ui.button("+").clicked() {
+                self.zoom = (self.zoom + 0.1).min(3.0);
+            }
+
+            ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
+                if ui.button("Close").clicked() {
+                    state.graph_instance = None;
+                    state.graph_relation = None;
+                    state.central_view = CentralView::EditorAndInspector;
+                }
+            });
+        });
+
+        ui.separator();
+
+        // Apply layout if needed
+        if self.needs_layout {
+            self.apply_layout(ui);
+            self.needs_layout = false;
+        }
+
+        // Draw the graph
+        self.draw_graph(ui);
+    }
+
+    fn show_selection_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
+        ui.label("Select an instance to visualize:");
+        ui.add_space(8.0);
+
+        let instances = state.repl.list_instances();
+        if instances.is_empty() {
+            ui.label("No instances defined.");
+        } else {
+            for instance in instances {
+                if ui.button(format!("{} : {}", instance.name, instance.theory_name)).clicked() {
+                    state.graph_instance = Some(instance.name.clone());
+                    self.needs_layout = true;
+                }
+            }
+        }
+
+        ui.add_space(16.0);
+        if ui.button("Back to Editor").clicked() {
+            state.central_view = CentralView::EditorAndInspector;
+        }
+    }
+
+    fn rebuild_graph(&mut self, state: &GuiState) {
+        self.nodes.clear();
+        self.edges.clear();
+        self.node_positions.clear();
+
+        let instance_name = match &state.graph_instance {
+            Some(name) => name,
+            None => return,
+        };
+
+        let entry = match state.repl.instances.get(instance_name) {
+            Some(e) => e,
+            None => return,
+        };
+
+        let theory = match state.repl.theories.get(&entry.theory_name) {
+            Some(t) => t,
+            None => return,
+        };
+
+        let sig = &theory.theory.signature;
+
+        // Create nodes for each element
+        let sort_colors = generate_sort_colors(sig.sorts.len());
+
+        for (slid_idx, &sort_id) in entry.structure.sorts.iter().enumerate() {
+            let slid = Slid::from_usize(slid_idx);
+            let name = entry
+                .slid_to_name
+                .get(&slid)
+                .map(|s| s.clone())
+                .unwrap_or_else(|| format!("#{}", slid_idx));
+
+            let sort_name = sig.sorts.get(sort_id).cloned().unwrap_or_default();
+            let color = sort_colors.get(sort_id).copied().unwrap_or(egui::Color32::GRAY);
+
+            self.nodes.push(GraphNode {
+                id: slid,
+                name,
+                sort: sort_name,
+                position: egui::Pos2::ZERO, // Will be set by layout
+                color,
+            });
+        }
+
+        // Create edges for relations
+        for (rel_id, relation) in entry.structure.relations.iter().enumerate() {
+            if relation.is_empty() {
+                continue;
+            }
+
+            let rel_name = sig
+                .relations
+                .get(rel_id)
+                .map(|r| r.name.clone())
+                .unwrap_or_else(|| format!("rel#{}", rel_id));
+
+            // Filter by selected relation
+            if let Some(selected) = &self.selected_relation {
+                if &rel_name != selected {
+                    continue;
+                }
+            }
+
+            for tuple in relation.iter() {
+                if tuple.len() >= 2 {
+                    // Binary or higher-arity relation: draw edge from first to last
+                    self.edges.push(GraphEdge {
+                        from: tuple[0],
+                        to: tuple[tuple.len() - 1],
+                        relation: rel_name.clone(),
+                        label: if tuple.len() > 2 {
+                            Some(format!("via {} elements", tuple.len() - 2))
+                        } else {
+                            None
+                        },
+                    });
+                } else if tuple.len() == 1 {
+                    // Unary relation: self-loop (or just highlight the node)
+                    self.edges.push(GraphEdge {
+                        from: tuple[0],
+                        to: tuple[0],
+                        relation: rel_name.clone(),
+                        label: None,
+                    });
+                }
+            }
+        }
+
+        self.last_instance = state.graph_instance.clone();
+        self.last_relation = state.graph_relation.clone();
+        self.needs_layout = true;
+    }
+
+    fn apply_layout(&mut self, _ui: &egui::Ui) {
+        if self.nodes.is_empty() {
+            return;
+        }
+
+        // Use a fixed coordinate system centered at (0, 0)
+        // The transform in draw_graph will handle screen positioning
+        let center = egui::Pos2::new(0.0, 0.0);
+
+        // Simple circular layout with fixed radius
+        let radius = 150.0;
+        let count = self.nodes.len();
+
+        for (i, node) in self.nodes.iter_mut().enumerate() {
+            let angle = (i as f32 / count as f32) * std::f32::consts::TAU;
+            let pos = egui::Pos2::new(
+                center.x + radius * angle.cos(),
+                center.y + radius * angle.sin(),
+            );
+            node.position = pos;
+            self.node_positions.insert(node.id, pos);
+        }
+    }
+
+    fn fit_to_view(&mut self, ui: &egui::Ui) {
+        if self.nodes.is_empty() {
+            return;
+        }
+
+        // Calculate bounding box of node positions (in world coordinates)
+        let mut min_x = f32::MAX;
+        let mut min_y = f32::MAX;
+        let mut max_x = f32::MIN;
+        let mut max_y = f32::MIN;
+
+        for node in &self.nodes {
+            let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
+            min_x = min_x.min(pos.x);
+            min_y = min_y.min(pos.y);
+            max_x = max_x.max(pos.x);
+            max_y = max_y.max(pos.y);
+        }
+
+        let width = (max_x - min_x).max(1.0);
+        let height = (max_y - min_y).max(1.0);
+        let available = ui.available_size();
+
+        // Calculate zoom to fit with padding
+        let padding = 100.0;
+        let zoom_x = (available.x - padding) / width;
+        let zoom_y = (available.y - padding) / height;
+        self.zoom = zoom_x.min(zoom_y).clamp(0.1, 2.0);
+
+        // Reset pan to center the content (since our world origin is already at center)
+        let world_center_x = (min_x + max_x) / 2.0;
+        let world_center_y = (min_y + max_y) / 2.0;
+        self.pan = egui::Vec2::new(
+            -world_center_x * self.zoom,
+            -world_center_y * self.zoom,
+        );
+    }
+
+    fn draw_graph(&mut self, ui: &mut egui::Ui) {
+        let (response, painter) = ui.allocate_painter(
+            ui.available_size(),
+            egui::Sense::click_and_drag(),
+        );
+
+        let rect = response.rect;
+
+        // Handle panning
+        if response.dragged() && self.dragged_node.is_none() {
+            self.pan += response.drag_delta();
+        }
+
+        // Handle zooming with scroll
+        if response.hovered() {
+            let scroll = ui.input(|i| i.raw_scroll_delta.y);
+            if scroll != 0.0 {
+                let old_zoom = self.zoom;
+                self.zoom = (self.zoom + scroll * 0.001).clamp(0.1, 3.0);
+
+                // Zoom toward mouse position
+                if let Some(pos) = response.hover_pos() {
+                    let rel_pos = pos - rect.min;
+                    let zoom_factor = self.zoom / old_zoom;
+                    self.pan = rel_pos - (rel_pos - self.pan) * zoom_factor;
+                }
+            }
+        }
+
+        // Transform helper - centers (0,0) world coordinates in the view
+        let center = rect.center();
+        let transform = |pos: egui::Pos2| -> egui::Pos2 {
+            egui::Pos2::new(
+                center.x + pos.x * self.zoom + self.pan.x,
+                center.y + pos.y * self.zoom + self.pan.y,
+            )
+        };
+
+        // Draw edges first (behind nodes)
+        for edge in &self.edges {
+            let from_pos = self.node_positions.get(&edge.from);
+            let to_pos = self.node_positions.get(&edge.to);
+
+            if let (Some(&from), Some(&to)) = (from_pos, to_pos) {
+                let from_screen = transform(from);
+                let to_screen = transform(to);
+
+                if edge.from == edge.to {
+                    // Self-loop
+                    let offset = 20.0 * self.zoom;
+                    let loop_center = egui::Pos2::new(from_screen.x, from_screen.y - offset);
+                    painter.circle_stroke(
+                        loop_center,
+                        10.0 * self.zoom,
+                        egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
+                    );
+                } else {
+                    // Regular edge
+                    painter.line_segment(
+                        [from_screen, to_screen],
+                        egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
+                    );
+
+                    // Draw arrowhead
+                    let dir = (to_screen - from_screen).normalized();
+                    let arrow_size = 8.0 * self.zoom;
+                    let node_radius = 20.0 * self.zoom;
+                    let arrow_tip = to_screen - dir * node_radius;
+                    let perp = egui::Vec2::new(-dir.y, dir.x);
+
+                    let p1 = arrow_tip;
+                    let p2 = arrow_tip - dir * arrow_size + perp * arrow_size * 0.5;
+                    let p3 = arrow_tip - dir * arrow_size - perp * arrow_size * 0.5;
+
+                    painter.add(egui::Shape::convex_polygon(
+                        vec![p1, p2, p3],
+                        egui::Color32::LIGHT_GRAY,
+                        egui::Stroke::NONE,
+                    ));
+                }
+            }
+        }
+
+        // Draw nodes
+        let node_radius = 20.0 * self.zoom;
+
+        for node in &self.nodes {
+            let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
+            let screen_pos = transform(pos);
+
+            // Check if node is being hovered or dragged
+            let node_rect = egui::Rect::from_center_size(
+                screen_pos,
+                egui::Vec2::splat(node_radius * 2.0),
+            );
+
+            let is_hovered = response.hovered()
+                && ui.input(|i| i.pointer.hover_pos())
+                    .map(|p| node_rect.contains(p))
+                    .unwrap_or(false);
+
+            // Handle node dragging
+            if is_hovered && response.drag_started() {
+                self.dragged_node = Some(node.id);
+            }
+
+            if self.dragged_node == Some(node.id) {
+                if response.dragged() {
+                    let delta = response.drag_delta() / self.zoom;
+                    if let Some(pos) = self.node_positions.get_mut(&node.id) {
+                        *pos += delta;
+                    }
+                }
+                if response.drag_stopped() {
+                    self.dragged_node = None;
+                }
+            }
+
+            // Draw node circle
+            let fill_color = if is_hovered || self.dragged_node == Some(node.id) {
+                node.color.linear_multiply(1.3)
+            } else {
+                node.color
+            };
+
+            painter.circle_filled(screen_pos, node_radius, fill_color);
+            painter.circle_stroke(
+                screen_pos,
+                node_radius,
+                egui::Stroke::new(2.0, egui::Color32::WHITE),
+            );
+
+            // Draw node label
+            let font_size = (12.0 * self.zoom).max(8.0);
+            painter.text(
+                screen_pos,
+                egui::Align2::CENTER_CENTER,
+                &node.name,
+                egui::FontId::proportional(font_size),
+                egui::Color32::WHITE,
+            );
+
+            // Draw sort label below
+            if is_hovered {
+                painter.text(
+                    screen_pos + egui::Vec2::new(0.0, node_radius + 5.0),
+                    egui::Align2::CENTER_TOP,
+                    &node.sort,
+                    egui::FontId::proportional(10.0 * self.zoom),
+                    egui::Color32::LIGHT_GRAY,
+                );
+            }
+        }
+
+        // Show info panel
+        if self.nodes.is_empty() {
+            painter.text(
+                rect.center(),
+                egui::Align2::CENTER_CENTER,
+                "No elements to display",
+                egui::FontId::proportional(16.0),
+                egui::Color32::GRAY,
+            );
+        }
+    }
+}
+
+impl Default for GraphView {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Generate distinct colors for each sort
+fn generate_sort_colors(count: usize) -> Vec<egui::Color32> {
+    let mut colors = Vec::with_capacity(count);
+
+    for i in 0..count {
+        let hue = (i as f32 / count as f32) * 360.0;
+        let (r, g, b) = hsv_to_rgb(hue, 0.6, 0.8);
+        colors.push(egui::Color32::from_rgb(r, g, b));
+    }
+
+    colors
+}
+
+/// Convert HSV to RGB
+fn hsv_to_rgb(h: f32, s: f32, v: f32) -> (u8, u8, u8) {
+    let c = v * s;
+    let x = c * (1.0 - ((h / 60.0) % 2.0 - 1.0).abs());
+    let m = v - c;
+
+    let (r, g, b) = if h < 60.0 {
+        (c, x, 0.0)
+    } else if h < 120.0 {
+        (x, c, 0.0)
+    } else if h < 180.0 {
+        (0.0, c, x)
+    } else if h < 240.0 {
+        (0.0, x, c)
+    } else if h < 300.0 {
+        (x, 0.0, c)
+    } else {
+        (c, 0.0, x)
+    };
+
+    (
+        ((r + m) * 255.0) as u8,
+        ((g + m) * 255.0) as u8,
+        ((b + m) * 255.0) as u8,
+    )
+}

src/gui/visualizations/mod.rs

@@ -0,0 +1,7 @@
+//! Visualization components for the Geolog GUI
+
+pub mod chase;
+pub mod graph;
+
+pub use chase::ChaseVisualization;
+pub use graph::GraphView;

src/lib.rs

@@ -6,6 +6,7 @@
 pub mod ast;
 pub mod cc;
 pub mod core;
+pub mod debugger;
 pub mod elaborate;
 pub mod error;
 pub mod id;
@@ -26,6 +27,9 @@ pub mod universe;
 pub mod version;
 pub mod zerocopy;
 
+#[cfg(feature = "gui")]
+pub mod gui;
+
 pub use ast::*;
 pub use lexer::lexer;
 pub use parser::parser;

src/query/chase.rs

@@ -84,6 +84,46 @@ impl std::error::Error for ChaseError {}
 /// Variable binding: maps variable names to Slids
 pub type Binding = HashMap<String, Slid>;
 
+/// Events emitted during chase execution
+#[derive(Clone, Debug)]
+pub enum ChaseEvent<'a> {
+    IterationStart { iteration: usize },
+    AxiomFiring {
+        axiom_index: usize,
+        axiom_name: Option<&'a str>,
+        binding: &'a Binding,
+        violation_count: usize,
+    },
+    AxiomFired {
+        axiom_index: usize,
+        axiom_name: Option<&'a str>,
+        changed: bool,
+    },
+    IterationEnd { iteration: usize, changed: bool },
+    ChaseComplete { iterations: usize },
+}
+
+/// Control signal returned by observer to control chase execution
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum ChaseControl {
+    Continue,
+    Stop,
+}
+
+/// Observer trait for monitoring chase execution
+pub trait ChaseObserver {
+    fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl;
+}
+
+/// Null observer that does nothing (default for regular chase)
+pub struct NullObserver;
+
+impl ChaseObserver for NullObserver {
+    fn on_event(&mut self, _: ChaseEvent<'_>) -> ChaseControl {
+        ChaseControl::Continue
+    }
+}
+
 /// Execute one step of the chase algorithm.
 ///
 /// Iterates over all axioms, evaluates premises using the tensor system,
@@ -707,4 +747,149 @@ pub fn chase_fixpoint(
     Ok(iterations)
 }
 
+/// Run the chase algorithm with an observer for debugging/monitoring.
+///
+/// This is the instrumented version that calls `observer.on_event()` at key points:
+/// - Start of each iteration
+/// - Before firing each axiom (with binding)
+/// - After firing each axiom (with changed flag)
+/// - End of each iteration
+/// - Chase completion
+///
+/// The observer can return `ChaseControl::Stop` to halt execution early.
+///
+/// # Arguments
+///
+/// * `axioms` - The sequents (axioms) to apply
+/// * `axiom_names` - Names for axioms (for display in debugger)
+/// * `structure` - The structure to modify
+/// * `universe` - The universe for element creation
+/// * `sig` - The signature
+/// * `max_iterations` - Safety limit to prevent infinite loops
+/// * `observer` - The observer to receive events
+///
+/// # Returns
+///
+/// The number of iterations taken, or error if chase failed or was stopped.
+pub fn chase_fixpoint_with_observer<O: ChaseObserver>(
+    axioms: &[Sequent],
+    axiom_names: &[String],
+    structure: &mut Structure,
+    universe: &mut Universe,
+    sig: &Signature,
+    max_iterations: usize,
+    observer: &mut O,
+) -> Result<usize, ChaseError> {
+    let mut cc = CongruenceClosure::new();
+    let mut iterations = 0;
+
+    loop {
+        if iterations >= max_iterations {
+            return Err(ChaseError::MaxIterationsExceeded(max_iterations));
+        }
+
+        // Notify iteration start
+        if observer.on_event(ChaseEvent::IterationStart { iteration: iterations + 1 }) == ChaseControl::Stop {
+            return Ok(iterations);
+        }
+
+        let mut iteration_changed = false;
+
+        // Fire axiom conclusions with observer notifications
+        for (axiom_idx, axiom) in axioms.iter().enumerate() {
+            let axiom_name = axiom_names.get(axiom_idx).map(|n| n.as_str()).filter(|s| !s.is_empty());
+
+            // Check the axiom - if compilation fails due to unsupported patterns, skip silently
+            let violations = match check_sequent(axiom, structure, sig) {
+                Ok(CheckResult::Satisfied) => continue,
+                Ok(CheckResult::Violated(vs)) => vs,
+                Err(_) => continue,
+            };
+
+            if violations.is_empty() {
+                continue;
+            }
+
+            // Build index→Slid lookup for each context variable
+            let index_to_slid: Vec<Vec<Slid>> = axiom.context.vars.iter()
+                .map(|(_, sort)| carrier_to_slid_vec(structure, sort))
+                .collect();
+
+            // Map from variable name to its position in the context
+            let var_to_ctx_idx: HashMap<&str, usize> = axiom.context.vars.iter()
+                .enumerate()
+                .map(|(i, (name, _))| (name.as_str(), i))
+                .collect();
+
+            // Fire conclusion for each violation
+            for violation in &violations {
+                // Build binding from violation assignment
+                let binding: Binding = violation.variable_names.iter()
+                    .enumerate()
+                    .filter_map(|(tensor_idx, var_name)| {
+                        let ctx_idx = var_to_ctx_idx.get(var_name.as_str())?;
+                        let slid_vec = &index_to_slid[*ctx_idx];
+                        let tensor_val = violation.assignment.get(tensor_idx)?;
+                        let slid = slid_vec.get(*tensor_val)?;
+                        Some((var_name.clone(), *slid))
+                    })
+                    .collect();
+
+                // Notify before firing
+                if observer.on_event(ChaseEvent::AxiomFiring {
+                    axiom_index: axiom_idx,
+                    axiom_name,
+                    binding: &binding,
+                    violation_count: violations.len(),
+                }) == ChaseControl::Stop {
+                    return Ok(iterations);
+                }
+
+                // Fire conclusion with this binding
+                let changed = match fire_conclusion(&axiom.conclusion, &binding, structure, &mut cc, universe, sig) {
+                    Ok(c) => c,
+                    Err(_) => false, // Skip unsupported conclusions
+                };
+
+                iteration_changed |= changed;
+
+                // Notify after firing
+                if observer.on_event(ChaseEvent::AxiomFired {
+                    axiom_index: axiom_idx,
+                    axiom_name,
+                    changed,
+                }) == ChaseControl::Stop {
+                    return Ok(iterations);
+                }
+            }
+        }
+
+        // Propagate pending equations in CC
+        let eq_changed = propagate_equations(structure, &mut cc, sig);
+        iteration_changed |= eq_changed;
+
+        iterations += 1;
+
+        // Notify iteration end
+        if observer.on_event(ChaseEvent::IterationEnd {
+            iteration: iterations,
+            changed: iteration_changed,
+        }) == ChaseControl::Stop {
+            return Ok(iterations);
+        }
+
+        if !iteration_changed {
+            break;
+        }
+    }
+
+    // Canonicalize structure to reflect CC merges
+    canonicalize_structure(structure, &mut cc);
+
+    // Notify chase completion
+    observer.on_event(ChaseEvent::ChaseComplete { iterations });
+
+    Ok(iterations)
+}
+
 // Tests are in tests/unit_chase.rs

src/repl.rs

@@ -1279,6 +1279,9 @@ pub enum MetaCommand {
     /// Chase: run chase algorithm on instance to compute derived relations/functions
     /// `:chase <instance> [max_iterations]`
     Chase { instance: String, max_iterations: Option<usize> },
+    /// DebugChase: run chase with interactive debugger
+    /// `:debug-chase <instance> [max_iterations]`
+    DebugChase { instance: String, max_iterations: Option<usize> },
     Unknown(String),
 }
 
@@ -1436,6 +1439,17 @@ impl MetaCommand {
                     MetaCommand::Unknown(":chase requires <instance> [max_iterations]".to_string())
                 }
             }
+            "debug-chase" => {
+                if let Some(instance_name) = arg {
+                    let max_iterations = parts.next().and_then(|s| s.parse().ok());
+                    MetaCommand::DebugChase {
+                        instance: instance_name.to_string(),
+                        max_iterations,
+                    }
+                } else {
+                    MetaCommand::Unknown(":debug-chase requires <instance> [max_iterations]".to_string())
+                }
+            }
             other => MetaCommand::Unknown(format!("Unknown command: :{}", other)),
         }
     }

tests/unit_chase.rs

@@ -3,8 +3,9 @@
 use geolog::core::{
     Context, DerivedSort, Formula, RelationStorage, Sequent, Signature, Structure, Term, Theory,
 };
-use geolog::query::chase::chase_fixpoint;
+use geolog::query::chase::{chase_fixpoint, chase_fixpoint_with_observer, ChaseEvent, ChaseControl, ChaseObserver};
 use geolog::universe::Universe;
+use std::collections::HashMap;
 
 /// Create a simple test theory with one sort and one unary relation
 fn simple_theory_with_relation() -> Theory {
@@ -424,3 +425,142 @@ fn test_chase_existential_premise() {
 
     println!("Chase with existential premise completed in {} iterations", iterations);
 }
+
+/// A test observer that counts events
+struct CountingObserver {
+    iteration_starts: usize,
+    axiom_firings: usize,
+    axiom_fired: usize,
+    iteration_ends: usize,
+    complete: usize,
+    last_binding: Option<HashMap<String, geolog::id::Slid>>,
+}
+
+impl CountingObserver {
+    fn new() -> Self {
+        Self {
+            iteration_starts: 0,
+            axiom_firings: 0,
+            axiom_fired: 0,
+            iteration_ends: 0,
+            complete: 0,
+            last_binding: None,
+        }
+    }
+}
+
+impl ChaseObserver for CountingObserver {
+    fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl {
+        match event {
+            ChaseEvent::IterationStart { .. } => self.iteration_starts += 1,
+            ChaseEvent::AxiomFiring { binding, .. } => {
+                self.axiom_firings += 1;
+                self.last_binding = Some(binding.clone());
+            }
+            ChaseEvent::AxiomFired { .. } => self.axiom_fired += 1,
+            ChaseEvent::IterationEnd { .. } => self.iteration_ends += 1,
+            ChaseEvent::ChaseComplete { .. } => self.complete += 1,
+        }
+        ChaseControl::Continue
+    }
+}
+
+#[test]
+fn test_chase_with_observer() {
+    // Test that the observer-based chase works and receives events
+    let theory = preorder_theory();
+    let mut universe = Universe::new();
+    let mut structure = Structure::new(1);
+
+    // Add 2 elements
+    structure.add_element(&mut universe, 0);
+    structure.add_element(&mut universe, 0);
+
+    // Initialize relation with arity 2
+    structure.init_relations(&[2]);
+
+    let mut observer = CountingObserver::new();
+
+    let iterations = chase_fixpoint_with_observer(
+        &theory.axioms,
+        &theory.axiom_names,
+        &mut structure,
+        &mut universe,
+        &theory.signature,
+        100,
+        &mut observer,
+    ).unwrap();
+
+    // Should complete with events
+    assert_eq!(iterations, 2);
+    assert!(observer.iteration_starts >= 1, "Should have at least 1 iteration start");
+    assert!(observer.axiom_firings >= 2, "Should have at least 2 axiom firings (reflexivity for 2 elements)");
+    assert_eq!(observer.complete, 1, "Should have exactly 1 completion event");
+
+    // Check that reflexive pairs were added
+    let relation = structure.get_relation(0);
+    assert_eq!(relation.len(), 2, "Should have 2 reflexive tuples");
+}
+
+/// An observer that stops after a fixed number of firings
+struct StoppingObserver {
+    max_firings: usize,
+    firing_count: usize,
+}
+
+impl StoppingObserver {
+    fn new(max_firings: usize) -> Self {
+        Self {
+            max_firings,
+            firing_count: 0,
+        }
+    }
+}
+
+impl ChaseObserver for StoppingObserver {
+    fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl {
+        if let ChaseEvent::AxiomFiring { .. } = event {
+            self.firing_count += 1;
+            if self.firing_count >= self.max_firings {
+                return ChaseControl::Stop;
+            }
+        }
+        ChaseControl::Continue
+    }
+}
+
+#[test]
+fn test_chase_observer_can_stop() {
+    // Test that returning ChaseControl::Stop halts the chase
+    let theory = preorder_theory();
+    let mut universe = Universe::new();
+    let mut structure = Structure::new(1);
+
+    // Add 5 elements - would normally produce 5 reflexive pairs
+    for _ in 0..5 {
+        structure.add_element(&mut universe, 0);
+    }
+
+    // Initialize relation with arity 2
+    structure.init_relations(&[2]);
+
+    // Stop after just 2 firings
+    // Note: The stop happens when the 2nd firing event is received, before the 2nd tuple is added
+    // So we expect only 1 tuple (from the first firing)
+    let mut observer = StoppingObserver::new(2);
+
+    let _iterations = chase_fixpoint_with_observer(
+        &theory.axioms,
+        &theory.axiom_names,
+        &mut structure,
+        &mut universe,
+        &theory.signature,
+        100,
+        &mut observer,
+    ).unwrap();
+
+    // Should have stopped early - only 1 tuple (the 2nd firing was interrupted before execution)
+    let relation = structure.get_relation(0);
+    assert!(relation.len() < 5, "Should have fewer than 5 tuples after early stop");
+    assert_eq!(observer.firing_count, 2, "Should have stopped after exactly 2 firings");
+}

tests/unit_debugger.rs

@@ -0,0 +1,93 @@
+//! Unit tests for the chase debugger
+
+use std::collections::HashMap;
+use geolog::debugger::InteractiveDebugger;
+use geolog::id::{NumericId, Slid};
+use geolog::query::chase::{Binding, ChaseControl, ChaseEvent, ChaseObserver};
+
+/// Test that format_binding correctly displays bindings with element names
+#[test]
+fn test_format_binding_with_names() {
+    let mut slid_to_name: HashMap<Slid, String> = HashMap::new();
+    slid_to_name.insert(Slid::from_usize(0), "alice".to_string());
+    slid_to_name.insert(Slid::from_usize(1), "bob".to_string());
+    slid_to_name.insert(Slid::from_usize(2), "charlie".to_string());
+
+    let axiom_names: Vec<String> = vec!["ax/test".to_string()];
+    let debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names);
+
+    let mut binding: Binding = HashMap::new();
+    binding.insert("x".to_string(), Slid::from_usize(0));
+    binding.insert("y".to_string(), Slid::from_usize(1));
+
+    let formatted = debugger.format_binding(&binding);
+
+    // Should contain both variable bindings with element names
+    assert!(formatted.contains("x=alice"), "Should contain x=alice, got: {}", formatted);
+    assert!(formatted.contains("y=bob"), "Should contain y=bob, got: {}", formatted);
+}
+
+/// Test that format_binding handles unknown elements gracefully
+#[test]
+fn test_format_binding_unknown_elements() {
+    let slid_to_name: HashMap<Slid, String> = HashMap::new(); // Empty - no names
+    let axiom_names: Vec<String> = vec![];
+    let debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names);
+
+    let mut binding: Binding = HashMap::new();
+    binding.insert("x".to_string(), Slid::from_usize(42));
+
+    let formatted = debugger.format_binding(&binding);
+
+    // Should show "?" for unknown element
+    assert!(formatted.contains("x=?"), "Should contain x=? for unknown element, got: {}", formatted);
+}
+
+/// Test that format_binding handles empty bindings
+#[test]
+fn test_format_binding_empty() {
+    let slid_to_name: HashMap<Slid, String> = HashMap::new();
+    let axiom_names: Vec<String> = vec![];
+    let debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names);
+
+    let binding: Binding = HashMap::new();
+    let formatted = debugger.format_binding(&binding);
+
+    assert_eq!(formatted, "(empty)");
+}
+
+/// Test that observer responds to iteration events
+#[test]
+fn test_debugger_iteration_events() {
+    let slid_to_name: HashMap<Slid, String> = HashMap::new();
+    let axiom_names: Vec<String> = vec!["ax/refl".to_string()];
+    let mut debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names);
+
+    // Iteration start should continue
+    let result = debugger.on_event(ChaseEvent::IterationStart { iteration: 1 });
+    assert_eq!(result, ChaseControl::Continue);
+
+    // Iteration end should continue (in default step mode, but no prompt in test)
+    let result = debugger.on_event(ChaseEvent::IterationEnd { iteration: 1, changed: false });
+    assert_eq!(result, ChaseControl::Continue);
+
+    // Chase complete should continue
+    let result = debugger.on_event(ChaseEvent::ChaseComplete { iterations: 1 });
+    assert_eq!(result, ChaseControl::Continue);
+}
+
+/// Test that axiom fired events are handled
+#[test]
+fn test_debugger_axiom_fired_event() {
+    let slid_to_name: HashMap<Slid, String> = HashMap::new();
+    let axiom_names: Vec<String> = vec!["ax/refl".to_string()];
+    let mut debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names);
+
+    // AxiomFired should always continue (it's informational)
+    let result = debugger.on_event(ChaseEvent::AxiomFired {
+        axiom_index: 0,
+        axiom_name: Some("ax/refl"),
+        changed: true,
+    });
+    assert_eq!(result, ChaseControl::Continue);
+}