Add scaffolding for SQL support

AGENTS.md

@@ -6,7 +6,7 @@ This file provides guidance to coding agents collaborating on this repository.
 
 Query Engine is an experimental Rust project for building query-engine
 components. The current implementation is centered on a chase-based reasoning
-core plus lightweight interactive frontends.
+core, lightweight interactive frontends, and an early relational/SQL scaffold.
 
 Priorities, in order:
 
@@ -52,8 +52,14 @@ Quick examples:
     - `rule.rs`: TGDs, EGDs, equalities, and builders.
     - `substitution.rs`: variable bindings and unification.
     - `engine.rs`: chase execution and configuration.
+    - `inference.rs`: shared matching and provenance-aware materialization helpers.
     - `union_find.rs`: equality merging support.
 - `src/frontend/`: lightweight interactive surface for scripts, REPL, and local web UI.
+- `src/relational/`: schemas, values, rows, and result sets for relational execution.
+- `src/catalog/`: predicate-to-table schema inference and catalog access.
+- `src/sql/`: narrow SQL AST and parser support.
+- `src/planner/`: logical plan structures and SQL-to-plan translation.
+- `src/execution/`: execution of the current logical plan subset.
 - `tests/`: integration, regression, and property-based tests.
 
 ## Architecture Constraints
@@ -64,6 +70,8 @@ Quick examples:
 - The chase engine should remain largely stateless; pass execution state explicitly.
 - New chase variants should be composable with existing infrastructure.
 - Existential variables generate labeled nulls (`Term::Null`).
+- The current SQL support is intentionally narrow: single-table `SELECT-FROM-WHERE` with positional column names such as `c0` and `c1`.
+- Relational and SQL modules should build on explicit schemas and logical plans, not call frontend helpers directly.
 - If you add parser, planner, or executor layers, keep their responsibilities separate.
 - Public docs and interfaces should reflect the implemented state of the repository accurately.
 
@@ -105,6 +113,7 @@ Example scopes that are good first tasks:
 - Implement a new utility method on `Instance` or `Atom`.
 - Tighten frontend wording so it matches actual behavior.
 - Introduce a small planning-oriented type without changing execution semantics.
+- Extend the SQL slice with a narrow, well-tested feature such as aliases or named columns.
 
 ## Testing Expectations
 
@@ -113,6 +122,7 @@ Example scopes that are good first tasks:
 - Integration tests go in `tests/integration_tests.rs`.
 - Regression tests for bug fixes go in `tests/regression_tests.rs`.
 - Property-based tests go in `tests/property_tests.rs`.
+- SQL/planner/execution flow tests go in `tests/sql_pipeline_tests.rs`.
 - Do not merge code that breaks existing tests.
 
 Minimal unit-test checklist for chase-related behavior:
@@ -151,6 +161,7 @@ Before coding:
 2. Identify affected tests.
 3. Consider impact on API stability.
 4. Avoid overstating roadmap progress in code comments or docs.
+5. Keep the supported SQL subset explicit when touching `sql`, `planner`, or `execution`.
 
 Before submitting:
 
@@ -186,6 +197,7 @@ Use this review format:
 - If you detect contradictory repository conventions, follow existing code and update docs accordingly.
 - When uncertain about correctness, add or extend tests first, then optimize.
 - When adding non-chase engine pieces, define clean interfaces before broadening functionality.
+- Keep `frontend` presentation-only when possible; shared reasoning logic belongs in `chase`, relational logic in `relational`/`planner`/`execution`.
 - Keep user-facing naming consistent with the repository name: `query-engine` / `query_engine`.
 
 ## Commit and PR Hygiene

ROADMAP.md

@@ -23,6 +23,12 @@ This document tracks the current state and next steps for the repository.
 - [x] Equality merging with union-find support
 - [x] REPL, script runner, and local web UI
 - [x] Provenance-oriented explanation support
+- [x] Relational schema, value, row, and result-set scaffolding
+- [x] Predicate-backed catalog inference
+- [x] Minimal SQL AST and parser
+- [x] Logical plan scaffolding
+- [x] Logical-plan execution for the first SQL slice
+- [x] Single-table `SELECT-FROM-WHERE` support with positional columns (`c0`, `c1`, ...)
 
 ### Near-Term Cleanup
 
@@ -30,27 +36,31 @@ This document tracks the current state and next steps for the repository.
 - [ ] Remove remaining stale terminology in comments and help text
 - [ ] Expand examples for the current rule-engine workflow
 - [ ] Add rustdoc coverage for the main public types
+- [ ] Document the current SQL subset and its limits
 
 ### Query-Engine Structure
 
-- [ ] Introduce a dedicated logical representation module
+- [x] Introduce a dedicated logical representation module
-- [ ] Define clear front-end, planning, and execution boundaries
+- [x] Define clear front-end, planning, and execution boundaries
 - [ ] Add engine-level abstractions that are not chase-specific
-- [ ] Establish common schema and typed-value representations
+- [x] Establish common schema and typed-value representations
 - [ ] Design a source boundary for future scans and pushdown
 
 ### Front End and Planning
 
-- [ ] Add a parser-oriented module beyond the current rule REPL language
+- [x] Add a parser-oriented module beyond the current rule REPL language
-- [ ] Add AST types for a structured query front end
+- [x] Add AST types for a structured query front end
-- [ ] Add logical plan node types
+- [x] Add logical plan node types
-- [ ] Add name resolution and schema validation hooks
+- [x] Add name resolution and schema validation hooks
-- [ ] Add expression typing and nullability tracking
+- [x] Add expression typing and nullability tracking
+- [ ] Add aliases and richer projection expressions
+- [ ] Add joins across multiple predicate-backed tables
+- [ ] Add a catalog path for stable column naming beyond `c0`, `c1`, ...
 
 ### Execution and Optimization
 
 - [ ] Introduce physical operator abstractions
-- [ ] Add a planning step from logical operators to executable operators
+- [x] Add a planning step from logical operators to executable operators
 - [ ] Add basic rule-based logical rewrites
 - [ ] Add statistics and cost-model scaffolding
 - [ ] Add indexing and access-path abstractions
@@ -73,7 +83,7 @@ This document tracks the current state and next steps for the repository.
 
 - [ ] Fact import/export
 - [ ] File-backed data source experiments
-- [ ] Table-like row or batch abstractions
+- [x] Table-like row or batch abstractions
 - [ ] Stable script/query file format
 - [ ] Integration with external storage or file formats
 
@@ -91,6 +101,7 @@ This document tracks the current state and next steps for the repository.
 - [x] Integration tests
 - [x] Property-based tests
 - [x] Regression tests
+- [x] Initial SQL pipeline tests
 - [ ] Benchmark coverage
 - [ ] Snapshot-style frontend tests
 - [ ] More planner/executor tests as those layers are added

examples/geolog/README.md

@@ -0,0 +1,529 @@
+# Geolog DSL Structure
+
+This directory contains example `.geolog` files that use a richer DSL than the
+minimal `.chase` script language in `examples/scripts/`.
+
+This README summarizes the Geolog DSL structure as it appears in the examples in
+this directory. It should be read as a practical, example-driven reference, not
+as a formal or complete language specification.
+
+## At a Glance
+
+- Top-level declarations are `theory` and `instance`.
+- The main kind of type is `Sort`.
+- Symbols can denote sorts, constants, functions, predicates, or nested
+  instances.
+- Axioms use sequent-style syntax: `premise |- conclusion`.
+- Instance bodies can be plain literals (`= { ... }`) or chase blocks
+  (`= chase { ... }`).
+- Function application is postfix, and qualified names use `/`.
+
+## Informal File Shape
+
+```text
+file := { comment | theory_decl | instance_decl }
+
+comment := // ...
+
+theory_decl :=
+  theory theory_params? Name {
+    theory_item*
+  }
+
+instance_decl :=
+  instance Name : theory_app = {
+    instance_item*
+  }
+
+  | instance Name : theory_app = chase {
+      instance_item*
+    }
+```
+
+In practice, a file is usually a sequence of theory declarations followed by one
+or more example instances.
+
+## Top-Level Declarations
+
+### `theory`
+
+A theory introduces sorts, symbols, and axioms.
+
+```text
+theory Graph {
+  V : Sort;
+  Edge : [src: V, tgt: V] -> Prop;
+}
+```
+
+Theories may also be parameterized.
+
+```text
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+}
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+```
+
+Observed parameter forms:
+
+- sort parameters: `(X : Sort)`
+- instance parameters: `(N : PetriNet instance)`
+- dependent instance parameters: `(RP : N ReachabilityProblem instance)`
+
+### `instance`
+
+An instance provides concrete elements and assignments for a theory.
+
+```text
+instance Triangle : Graph = {
+  A : V;
+  B : V;
+  C : V;
+}
+```
+
+Instances may target parameterized theories by writing the arguments before the
+theory name.
+
+```text
+instance MyMap : MyBase Map = { ... }
+instance solution0 : ExampleNet problem0 Solution = { ... }
+instance AB_Iso : As/a Bs/b Iso = { ... }
+```
+
+## Theory Body Items
+
+The examples show the following declaration forms inside a theory body.
+
+### Sort declarations
+
+```text
+V : Sort;
+E : Sort;
+```
+
+This introduces carrier sorts.
+
+### Constants or distinguished elements
+
+```text
+elem : X;
+```
+
+This introduces a named element of an existing sort.
+
+### Functions
+
+```text
+src : E -> V;
+fwd : X -> Y;
+token/of : token -> N/P;
+```
+
+Names may contain `/`, which is used heavily for structured or qualified names.
+
+### Predicates and relations
+
+Unary predicates:
+
+```text
+completed : Item -> Prop;
+```
+
+Record-shaped predicates:
+
+```text
+Edge : [src: V, tgt: V] -> Prop;
+depends : [item: Item, on: Item] -> Prop;
+```
+
+### Product-valued functions
+
+Functions may return record-shaped values.
+
+```text
+pair_of : A -> [left: B, right: C];
+W/src : W -> [firing: F, arc: N/out];
+```
+
+### Nested instance slots
+
+Theories can contain fields whose values are themselves instances.
+
+```text
+initial_marking : N Marking instance;
+trace : N Trace instance;
+initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+```
+
+### Axioms
+
+Axioms use a sequent-like form.
+
+```text
+ax/trans : forall x, y, z : V.
+  [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path;
+```
+
+An axiom declaration has the observed structure:
+
+```text
+name : forall binders. premise |- conclusion;
+```
+
+## Formula and Term Syntax
+
+The examples use the following building blocks inside axioms and assignments.
+
+### Quantifiers
+
+Universal binders appear after `forall`.
+
+```text
+forall x : X, y : Y.
+```
+
+Existentials appear directly inside conclusions or disjuncts.
+
+```text
+exists r : R. r R/data = [x: a, y: b]
+exists w : W. w W/src_firing = f, w W/src_arc = arc
+```
+
+### Sequents
+
+The central connective is `|-`, separating premise from conclusion.
+
+```text
+premise1, premise2 |- conclusion1, conclusion2;
+```
+
+In the examples:
+
+- commas act as conjunctions
+- the left side is the premise
+- the right side is the conclusion
+
+### Equality
+
+Equality is used for ordinary values and compound values.
+
+```text
+ab src = A
+r R/data = [x: a, y: b]
+x fwd bwd = x
+```
+
+### Truth constants
+
+```text
+|- true;
+|- false;
+```
+
+### Disjunction
+
+Disjunction is written as `\/`.
+
+```text
+[item: x, on: y] depends |- x blocked \/ y completed;
+```
+
+### Predicate atoms
+
+Unary predicate atoms:
+
+```text
+x blocked
+y completed
+```
+
+Record-shaped predicate atoms:
+
+```text
+[src: x, tgt: y] Edge
+[a: x, f: i] id
+```
+
+### Postfix application
+
+Function application is postfix and can be chained.
+
+```text
+e src
+x id
+x fwd bwd
+w W/src_arc N/out/tgt
+```
+
+This is one of the most distinctive traits of the DSL.
+
+### Qualified paths
+
+The slash `/` is used for qualification and nested access.
+
+Observed examples include:
+
+```text
+R/data
+N/P
+N/out/src
+trace/input_terminal
+RP/initial_marking/token
+ExampleNet/A
+```
+
+### Record literals
+
+Records are written with brackets and named fields.
+
+```text
+[x: a, y: b]
+[firing: f, arc: arc]
+```
+
+The examples also show positional shorthand for record arguments when the field
+order is known:
+
+```text
+[e, e] mul = e;
+[cook_dinner, on: buy_groceries] depends;
+```
+
+### Field projection
+
+Record-valued terms support field projection.
+
+```text
+r R/data .x = a
+```
+
+## Instance Body Items
+
+The examples show the following forms inside instance bodies.
+
+### Element declarations
+
+```text
+a : V;
+tok : token;
+ab : T;
+```
+
+### Function assignments
+
+```text
+ab src = A;
+tok token/of = ExampleNet/A;
+a1 map = MyBase/b1;
+```
+
+### Predicate facts
+
+Unary facts:
+
+```text
+buy_groceries completed;
+```
+
+Record-shaped facts:
+
+```text
+[src: a, tgt: b] Edge;
+[item: x, on: y] depends;
+```
+
+### Product-valued assignments
+
+```text
+a1 pair_of = [left: b1, right: c1];
+ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
+```
+
+### Nested instance literals
+
+Instance-valued fields can be assigned inline blocks.
+
+```text
+initial_marking = {
+  tok : token;
+  tok token/of = ExampleNet/A;
+};
+```
+
+## `= { ... }` vs `= chase { ... }`
+
+The examples consistently use two instance forms.
+
+### Plain instance
+
+```text
+instance Triangle : Graph = {
+  ...
+}
+```
+
+This gives a direct structure with only the explicitly listed elements and
+assignments.
+
+### Chase instance
+
+```text
+instance Chain : Graph = chase {
+  ...
+}
+```
+
+This marks an instance whose contents should be extended by the theory axioms.
+Examples use this for transitive closure, existential witness generation, and
+trace/reachability constructions.
+
+## Observed Design Patterns
+
+### Parameterized theories
+
+Theories can be abstract over:
+
+- a sort, such as `theory (X : Sort) Container`
+- an instance, such as `theory (N : PetriNet instance) Marking`
+- multiple arguments, such as `theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution`
+
+### Theory application by adjacency
+
+Theory arguments are written before the theory name.
+
+```text
+N Marking instance
+MyBase Map
+ExampleNet problem0 Solution
+```
+
+### Nested structure via qualified names
+
+Many examples model dependent structure by naming into earlier declarations.
+
+```text
+token/of : token -> N/P;
+initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+```
+
+## What Seems Outside the File DSL
+
+Some example comments refer to interactive commands such as:
+
+```text
+:source
+:load
+:inspect
+:chase
+:solve
+```
+
+Those commands appear to belong to an external REPL or tool environment rather
+than to the `.geolog` file grammar itself.
+
+## Querying
+
+The examples do **not** show a stable, implemented query form inside `.geolog`
+files in the same way they show `theory` and `instance` declarations.
+
+What they do show is:
+
+### 1. External interactive commands
+
+Some files suggest that querying or inspection happens through an external tool
+or REPL:
+
+```text
+:source examples/geolog/transitive_closure.geolog
+:inspect Chain
+:chase Chain
+:solve EmptyModel
+```
+
+Based on the example comments, these commands appear to mean roughly:
+
+- `:source` or `:load`: load Geolog definitions from files
+- `:inspect`: inspect a declared instance
+- `:chase`: materialize or display the closure of a `= chase` instance
+- `:solve`: ask a solver to construct a satisfying instance for a theory
+
+These are tool commands, not part of the confirmed `.geolog` declaration syntax.
+
+### 2. A sketched future query form
+
+One file contains a commented-out example of a possible query block:
+
+```text
+query can_reach_B_from_A {
+  ? : ExampleNet problem0 Solution instance;
+}
+```
+
+This suggests an aspirational style where querying is expressed as asking for a
+witness inhabiting some instance type. However, in the current examples this is
+only a comment, not an observed live construct.
+
+### 3. Current implemented querying elsewhere in the repo
+
+The currently implemented query syntax in this repository belongs to the minimal
+frontend language, not to Geolog. That language supports forms such as:
+
+```text
+query Ancestor(?X, ?Y)?
+explain Ancestor(alice, carol)?
+```
+
+So the safest summary is:
+
+- Geolog examples define theories, instances, and chase-oriented structure.
+- Querying appears to be external, REPL-driven, or still in design.
+- The only clearly implemented query syntax in this repo today is the minimal
+  `.chase` frontend query language.
+
+## Best Example Files by Feature
+
+- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage
+- `graph.geolog`: plain structural instances
+- `monoid.geolog`: postfix application and positional record syntax
+- `todo_list.geolog`: unary predicates and disjunction
+- `sort_param_simple.geolog`: sort and instance parameters
+- `nested_instance_test.geolog`: nested instance-valued fields
+- `product_codomain_test.geolog`: record-valued function codomains
+- `field_projection_test.geolog`: field projection syntax
+- `record_existential_test.geolog`: existential witness creation with records
+- `petri_net_showcase.geolog`: large multi-theory composition
+- `solver_demo.geolog`: satisfiability-oriented axiom patterns
+
+## Minimal Example
+
+```text
+theory Graph {
+  V : Sort;
+  Edge : [src: V, tgt: V] -> Prop;
+  Path : [src: V, tgt: V] -> Prop;
+
+  ax/base : forall x, y : V.
+    [src: x, tgt: y] Edge |- [src: x, tgt: y] Path;
+}
+
+instance Chain : Graph = chase {
+  a : V;
+  b : V;
+  [src: a, tgt: b] Edge;
+}
+```
+
+That small example already shows the core structure of the DSL:
+
+- a `theory`
+- sort and predicate declarations
+- an axiom written as a sequent
+- an `instance`
+- a `chase` block that asks for closure under the theory axioms

examples/geolog/category.geolog

@@ -0,0 +1,86 @@
+// Category theory in current geolog syntax
+//
+// This is the "desugared" version of the aspirational syntax in
+// loose_thoughts/2026-01-21_dependent_sorts_and_functional_relations.md
+
+theory Category {
+  ob : Sort;
+  mor : Sort;
+
+  // Morphism source and target
+  src : mor -> ob;
+  tgt : mor -> ob;
+
+  // Composition: comp(f, g, h) means "h = f ; g" (f then g)
+  // Domain constraint: f.tgt = g.src
+  comp : [f: mor, g: mor, h: mor] -> Prop;
+
+  // Identity: id(a, f) means "f is the identity on a"
+  id : [a: ob, f: mor] -> Prop;
+
+  // === Axioms ===
+
+  // Identity morphisms have matching source and target
+  ax/id_src : forall x : ob, i : mor. [a: x, f: i] id |- i src = x;
+  ax/id_tgt : forall x : ob, i : mor. [a: x, f: i] id |- i tgt = x;
+
+  // Composition domain constraint
+  ax/comp_dom : forall p : mor, q : mor, r : mor.
+    [f: p, g: q, h: r] comp |- p tgt = q src;
+
+  // Composition source/target
+  ax/comp_src : forall p : mor, q : mor, r : mor.
+    [f: p, g: q, h: r] comp |- r src = p src;
+  ax/comp_tgt : forall p : mor, q : mor, r : mor.
+    [f: p, g: q, h: r] comp |- r tgt = q tgt;
+
+  // Existence of identities (one per object)
+  ax/id_exists : forall x : ob. |- exists i : mor. [a: x, f: i] id;
+
+  // Existence of composites (when composable)
+  ax/comp_exists : forall p : mor, q : mor.
+    p tgt = q src |- exists r : mor. [f: p, g: q, h: r] comp;
+
+  // Left unit: id_a ; f = f
+  ax/unit_left : forall x : ob, i : mor, p : mor, r : mor.
+    [a: x, f: i] id, p src = x, [f: i, g: p, h: r] comp |- r = p;
+
+  // Right unit: f ; id_b = f
+  ax/unit_right : forall y : ob, i : mor, p : mor, r : mor.
+    [a: y, f: i] id, p tgt = y, [f: p, g: i, h: r] comp |- r = p;
+
+  // Associativity: (f ; g) ; h = f ; (g ; h)
+  ax/assoc : forall p : mor, q : mor, r : mor, pq : mor, qr : mor, pqr1 : mor, pqr2 : mor.
+    [f: p, g: q, h: pq] comp, [f: pq, g: r, h: pqr1] comp,
+    [f: q, g: r, h: qr] comp, [f: p, g: qr, h: pqr2] comp
+    |- pqr1 = pqr2;
+
+  // Uniqueness of composition (functional)
+  ax/comp_unique : forall p : mor, q : mor, r1 : mor, r2 : mor.
+    [f: p, g: q, h: r1] comp, [f: p, g: q, h: r2] comp |- r1 = r2;
+
+  // Uniqueness of identity (one per object)
+  ax/id_unique : forall x : ob, i1 : mor, i2 : mor.
+    [a: x, f: i1] id, [a: x, f: i2] id |- i1 = i2;
+}
+
+// The "walking arrow" category: A --f--> B
+//
+// Now we can declare just objects and non-identity morphisms!
+// The chase derives:
+// - Identity morphisms for each object (via ax/id_exists)
+// - Composition facts (via ax/comp_exists)
+// - Source/target for compositions (via ax/comp_src, ax/comp_tgt)
+//
+// The equality saturation (via congruence closure) collapses:
+// - id;id;id;... = id (via ax/unit_left and ax/unit_right)
+// - Duplicate compositions (via ax/comp_unique)
+// Without CC, the chase would loop forever creating id;id, id;id;id, ...
+instance Arrow : Category = chase {
+  // Objects
+  A : ob;
+  B : ob;
+
+  // Non-identity morphism
+  f : mor; f src = A; f tgt = B;
+}

examples/geolog/field_projection_chase_test.geolog

@@ -0,0 +1,27 @@
+// Test: Field projection in chase
+
+theory FieldProjectionChaseTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Marker sort for elements whose x field matches a given a
+  XMatches : Sort;
+  XMatches/r : XMatches -> R;
+  XMatches/a : XMatches -> A;
+
+  // Axiom: if r's x field equals a, create an XMatches
+  ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists m : XMatches. m XMatches/r = r, m XMatches/a = a;
+}
+
+instance Test : FieldProjectionChaseTest = chase {
+  a1 : A;
+  a2 : A;
+  b1 : B;
+  r1 : R;
+  r1 R/data = [x: a1, y: b1];
+  r2 : R;
+  r2 R/data = [x: a2, y: b1];
+}

examples/geolog/field_projection_test.geolog

@@ -0,0 +1,12 @@
+// Test: Field projection syntax
+
+theory FieldProjectionTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Axiom using field projection: r R/data .x
+  ax1 : forall r : R, a : A. r R/data .x = a |- true;
+}

examples/geolog/graph.geolog

@@ -0,0 +1,79 @@
+// Directed Graph: vertices and edges with source/target functions
+//
+// This is the canonical example of a "presheaf" - a functor from a small
+// category (the "walking arrow" • → •) to Set.
+
+theory Graph {
+  V : Sort;  // Vertices
+  E : Sort;  // Edges
+
+  src : E -> V;  // Source of an edge
+  tgt : E -> V;  // Target of an edge
+}
+
+// A simple triangle graph: A → B → C → A
+instance Triangle : Graph = {
+  // Vertices
+  A : V;
+  B : V;
+  C : V;
+
+  // Edges
+  ab : E;
+  bc : E;
+  ca : E;
+
+  // Edge endpoints
+  ab src = A;
+  ab tgt = B;
+  bc src = B;
+  bc tgt = C;
+  ca src = C;
+  ca tgt = A;
+}
+
+// A self-loop: one vertex with an edge to itself
+instance Loop : Graph = {
+  v : V;
+  e : E;
+  e src = v;
+  e tgt = v;
+}
+
+// The "walking arrow": two vertices, one edge
+instance Arrow : Graph = {
+  s : V;
+  t : V;
+  f : E;
+  f src = s;
+  f tgt = t;
+}
+
+// A more complex graph: diamond shape with two paths from top to bottom
+//
+//       top
+//      /   \
+//    left  right
+//      \   /
+//      bottom
+//
+instance Diamond : Graph = {
+  top : V;
+  left : V;
+  right : V;
+  bottom : V;
+
+  top_left : E;
+  top_right : E;
+  left_bottom : E;
+  right_bottom : E;
+
+  top_left src = top;
+  top_left tgt = left;
+  top_right src = top;
+  top_right tgt = right;
+  left_bottom src = left;
+  left_bottom tgt = bottom;
+  right_bottom src = right;
+  right_bottom tgt = bottom;
+}

examples/geolog/iso_instance_test.geolog

@@ -0,0 +1,29 @@
+// Multi-parameter theory instantiation test
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+theory A { a : Sort; }
+theory B { b : Sort; }
+
+instance As : A = {
+  a1 : a;
+  a2 : a;
+}
+
+instance Bs : B = {
+  b1 : b;
+  b2 : b;
+}
+
+// Can we create an Iso instance with sort parameters?
+instance AB_Iso : As/a Bs/b Iso = {
+  a1 fwd = Bs/b1;
+  a2 fwd = Bs/b2;
+  b1 bwd = As/a1;
+  b2 bwd = As/a2;
+}

examples/geolog/iso_theory_test.geolog

@@ -0,0 +1,9 @@
+// Multi-parameter theory test (Iso from vision)
+
+// First just try sorts as parameters
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  // Axioms would need chained function application...
+  // fb : forall x : X. |- x fwd bwd = x;
+}

examples/geolog/monoid.geolog

@@ -0,0 +1,78 @@
+// Monoid: a set with an associative binary operation and identity element
+//
+// This is the simplest algebraic structure with interesting axioms.
+// Note: geolog uses postfix function application.
+
+theory Monoid {
+  M : Sort;
+
+  // Binary operation: M × M → M
+  mul : [x: M, y: M] -> M;
+
+  // Identity element: we use a unary function from M to M that
+  // "picks out" the identity (any x maps to e)
+  // A cleaner approach would use Unit → M but that needs product support.
+  id : M -> M;
+
+  // Left identity: id(x) * y = y (id(x) is always e)
+  ax/left_id : forall x : M, y : M.
+    |- [x: x id, y: y] mul = y;
+
+  // Right identity: x * id(y) = x
+  ax/right_id : forall x : M, y : M.
+    |- [x: x, y: y id] mul = x;
+
+  // Associativity: (x * y) * z = x * (y * z)
+  ax/assoc : forall x : M, y : M, z : M.
+    |- [x: [x: x, y: y] mul, y: z] mul = [x: x, y: [x: y, y: z] mul] mul;
+
+  // id is constant: id(x) = id(y) for all x, y
+  ax/id_const : forall x : M, y : M.
+    |- x id = y id;
+}
+
+// Trivial monoid: single element, e * e = e
+instance Trivial : Monoid = {
+  e : M;
+
+  // Multiplication table: e * e = e
+  // Using positional syntax: [a, b] maps to [x: a, y: b]
+  [e, e] mul = e;
+
+  // Identity: e is the identity element
+  e id = e;
+}
+
+// Boolean "And" monoid: {T, F} with T as identity
+// T and T = T, T and F = F, F and T = F, F and F = F
+instance BoolAnd : Monoid = {
+  T : M;
+  F : M;
+
+  // Identity: T is the identity element
+  T id = T;
+  F id = T;
+
+  // Multiplication table for "and":
+  [x: T, y: T] mul = T;
+  [x: T, y: F] mul = F;
+  [x: F, y: T] mul = F;
+  [x: F, y: F] mul = F;
+}
+
+// Boolean "Or" monoid: {T, F} with F as identity
+// T or T = T, T or F = T, F or T = T, F or F = F
+instance BoolOr : Monoid = {
+  T : M;
+  F : M;
+
+  // Identity: F is the identity element
+  T id = F;
+  F id = F;
+
+  // Multiplication table for "or":
+  [x: T, y: T] mul = T;
+  [x: T, y: F] mul = T;
+  [x: F, y: T] mul = T;
+  [x: F, y: F] mul = F;
+}

examples/geolog/nested_instance_test.geolog

@@ -0,0 +1,33 @@
+// Test: Nested instance declarations (following vision pattern)
+
+theory Place {
+  P : Sort;
+}
+
+theory (Pl : Place instance) Token {
+  token : Sort;
+  token/of : token -> Pl/P;
+}
+
+theory (Pl : Place instance) Problem {
+  initial_marking : Pl Token instance;
+  target_marking : Pl Token instance;
+}
+
+// Create a place instance
+instance MyPlaces : Place = {
+  p1 : P;
+  p2 : P;
+}
+
+// Test nested instance declarations
+instance TestProblem : MyPlaces Problem = {
+  initial_marking = {
+    t1 : token;
+    t1 token/of = MyPlaces/p1;
+  };
+  target_marking = {
+    t2 : token;
+    t2 token/of = MyPlaces/p2;
+  };
+}

examples/geolog/petri_net.geolog

@@ -0,0 +1,135 @@
+// Petri Net: a bipartite graph between places and transitions
+//
+// Petri nets model concurrent systems. Places hold tokens, transitions
+// fire when their input places have tokens, consuming inputs and
+// producing outputs.
+//
+// This encoding uses explicit "arc" sorts for input/output connections,
+// which is more faithful to the categorical semantics (a span).
+
+theory PetriNet {
+  P : Sort;    // Places
+  T : Sort;    // Transitions
+  In : Sort;   // Input arcs (from place to transition)
+  Out : Sort;  // Output arcs (from transition to place)
+
+  // Input arc endpoints
+  in/place : In -> P;
+  in/trans : In -> T;
+
+  // Output arc endpoints
+  out/trans : Out -> T;
+  out/place : Out -> P;
+}
+
+// A simple producer-consumer net:
+//
+//   (ready) --[produce]--> (buffer) --[consume]--> (done)
+//
+instance ProducerConsumer : PetriNet = {
+  // Places
+  ready : P;
+  buffer : P;
+  done : P;
+
+  // Transitions
+  produce : T;
+  consume : T;
+
+  // Input arcs
+  i1 : In;
+  i1 in/place = ready;
+  i1 in/trans = produce;
+
+  i2 : In;
+  i2 in/place = buffer;
+  i2 in/trans = consume;
+
+  // Output arcs
+  o1 : Out;
+  o1 out/trans = produce;
+  o1 out/place = buffer;
+
+  o2 : Out;
+  o2 out/trans = consume;
+  o2 out/place = done;
+}
+
+// Mutual exclusion: two processes competing for a shared resource
+//
+//   (idle1) --[enter1]--> (crit1) --[exit1]--> (idle1)
+//                 ^                    |
+//                 |      (mutex)       |
+//                 |                    v
+//   (idle2) --[enter2]--> (crit2) --[exit2]--> (idle2)
+//
+instance MutualExclusion : PetriNet = {
+  // Places for process 1
+  idle1 : P;
+  crit1 : P;
+
+  // Places for process 2
+  idle2 : P;
+  crit2 : P;
+
+  // Shared mutex token
+  mutex : P;
+
+  // Transitions
+  enter1 : T;
+  exit1 : T;
+  enter2 : T;
+  exit2 : T;
+
+  // Process 1 enters: needs idle1 AND mutex
+  i_enter1_idle : In;
+  i_enter1_idle in/place = idle1;
+  i_enter1_idle in/trans = enter1;
+
+  i_enter1_mutex : In;
+  i_enter1_mutex in/place = mutex;
+  i_enter1_mutex in/trans = enter1;
+
+  o_enter1 : Out;
+  o_enter1 out/trans = enter1;
+  o_enter1 out/place = crit1;
+
+  // Process 1 exits: releases mutex
+  i_exit1 : In;
+  i_exit1 in/place = crit1;
+  i_exit1 in/trans = exit1;
+
+  o_exit1_idle : Out;
+  o_exit1_idle out/trans = exit1;
+  o_exit1_idle out/place = idle1;
+
+  o_exit1_mutex : Out;
+  o_exit1_mutex out/trans = exit1;
+  o_exit1_mutex out/place = mutex;
+
+  // Process 2 enters: needs idle2 AND mutex
+  i_enter2_idle : In;
+  i_enter2_idle in/place = idle2;
+  i_enter2_idle in/trans = enter2;
+
+  i_enter2_mutex : In;
+  i_enter2_mutex in/place = mutex;
+  i_enter2_mutex in/trans = enter2;
+
+  o_enter2 : Out;
+  o_enter2 out/trans = enter2;
+  o_enter2 out/place = crit2;
+
+  // Process 2 exits: releases mutex
+  i_exit2 : In;
+  i_exit2 in/place = crit2;
+  i_exit2 in/trans = exit2;
+
+  o_exit2_idle : Out;
+  o_exit2_idle out/trans = exit2;
+  o_exit2_idle out/place = idle2;
+
+  o_exit2_mutex : Out;
+  o_exit2_mutex out/trans = exit2;
+  o_exit2_mutex out/place = mutex;
+}

examples/geolog/petri_net_full.geolog

@@ -0,0 +1,195 @@
+// Full Petri Net Reachability - Type-Theoretic Encoding
+//
+// This demonstrates the complete type-theoretic encoding of Petri net
+// reachability from the original geolog design vision.
+//
+// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md
+//
+// Key concepts:
+// - PetriNet: places, transitions, input/output arcs (with proper arc semantics)
+// - Marking: tokens in a net (parameterized by net)
+// - ReachabilityProblem: initial and target markings (nested instances)
+// - Trace: sequence of firings with wires connecting arcs
+// - Iso: isomorphism between two sorts (used for bijections)
+// - Solution: a trace with isomorphisms to markings
+//
+// This encoding is more type-theoretically precise than the simple
+// PlaceReachability: it tracks individual tokens and arc multiplicities,
+// enabling correct handling of "multi-token" transitions.
+
+// ============================================================
+// THEORY: PetriNet
+// Basic structure: places, transitions, and arcs
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+
+  in : Sort;     // Input arcs (place -> transition)
+  out : Sort;    // Output arcs (transition -> place)
+
+  // Each arc knows which place/transition it connects
+  in/src : in -> P;    // Input arc source place
+  in/tgt : in -> T;    // Input arc target transition
+  out/src : out -> T;  // Output arc source transition
+  out/tgt : out -> P;  // Output arc target place
+}
+
+// ============================================================
+// THEORY: Marking (parameterized by N : PetriNet)
+// A marking assigns tokens to places
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+// ============================================================
+// THEORY: ReachabilityProblem (parameterized by N : PetriNet)
+// Defines initial and target markings as nested instances
+// ============================================================
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// ============================================================
+// THEORY: Trace (parameterized by N : PetriNet)
+// A trace is a sequence of transition firings with "wires"
+// connecting input and output arcs
+// ============================================================
+
+theory (N : PetriNet instance) Trace {
+  // Firings
+  F : Sort;
+  F/of : F -> N/T;
+
+  // Wires connect output of one firing to input of another
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];  // Wire source (firing, output arc)
+  W/tgt : W -> [firing : F, arc : N/in];   // Wire target (firing, input arc)
+
+  // Wire coherence: output arc must belong to source firing's transition
+  ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of;
+  // Wire coherence: input arc must belong to target firing's transition
+  ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of;
+
+  // Wire uniqueness: each (firing, out-arc) pair has at most one wire
+  ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+  // Wire uniqueness: each (firing, in-arc) pair has at most one wire
+  ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2;
+
+  // Terminals: for initial marking tokens (input) and final marking tokens (output)
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Every output arc of every firing must be wired OR be an output terminal
+  ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |-
+    (exists w : W. w W/src = [firing: f, arc: arc]) \/
+    (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+
+  // Every input arc of every firing must be wired OR be an input terminal
+  ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |-
+    (exists w : W. w W/tgt = [firing: f, arc: arc]) \/
+    (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]);
+}
+
+// ============================================================
+// THEORY: Iso (parameterized by two sorts)
+// An isomorphism between two sorts
+// ============================================================
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+// ============================================================
+// THEORY: Solution (parameterized by N and RP)
+// A solution to a reachability problem
+// ============================================================
+
+theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
+  // The witnessing trace
+  trace : N Trace instance;
+
+  // Bijection between input terminals and initial marking tokens
+  initial_marking_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+
+  // Bijection between output terminals and target marking tokens
+  target_marking_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
+
+  // Initial marking commutes: token placement matches terminal placement
+  initial_marking_P_comm : forall i : trace/input_terminal.
+    |- i trace/input_terminal/of = i initial_marking_iso/fwd RP/initial_marking/token/of;
+
+  // Target marking commutes: token placement matches terminal placement
+  target_marking_P_comm : forall o : trace/output_terminal.
+    |- o trace/output_terminal/of = o target_marking_iso/fwd RP/target_marking/token/of;
+}
+
+// ============================================================
+// INSTANCE: ExampleNet - a small Petri net
+//
+//   (A) --[ab]--> (B) --[bc]--> (C)
+//    ^             |
+//    +---[ba]------+
+// ============================================================
+
+instance ExampleNet : PetriNet = {
+  // Places
+  A : P;
+  B : P;
+  C : P;
+
+  // Transitions
+  ab : T;
+  ba : T;
+  bc : T;
+
+  // A -> B (via ab)
+  ab_in : in;
+  ab_in in/src = A;
+  ab_in in/tgt = ab;
+  ab_out : out;
+  ab_out out/src = ab;
+  ab_out out/tgt = B;
+
+  // B -> A (via ba)
+  ba_in : in;
+  ba_in in/src = B;
+  ba_in in/tgt = ba;
+  ba_out : out;
+  ba_out out/src = ba;
+  ba_out out/tgt = A;
+
+  // B -> C (via bc)
+  bc_in : in;
+  bc_in in/src = B;
+  bc_in in/tgt = bc;
+  bc_out : out;
+  bc_out out/src = bc;
+  bc_out out/tgt = C;
+}
+
+// ============================================================
+// Example queries (once query solving is implemented):
+//
+// query can_reach_B_from_A {
+//   ? : ExampleNet problem0 Solution instance;
+// }
+//
+// where problem0 : ExampleNet ReachabilityProblem = {
+//   initial_marking = { tok : token; tok token/of = ExampleNet/A; };
+//   target_marking = { tok : token; tok token/of = ExampleNet/B; };
+// }
+// ============================================================

examples/geolog/petri_net_showcase.geolog

@@ -0,0 +1,345 @@
+// Petri Net Reachability - Full Type-Theoretic Encoding
+//
+// This showcase demonstrates geolog's core capabilities through a
+// non-trivial domain: encoding Petri net reachability as dependent types.
+//
+// A solution to a reachability problem is NOT a yes/no boolean but a
+// CONSTRUCTIVE WITNESS: a diagrammatic proof that tokens can flow from
+// initial to target markings via a sequence of transition firings.
+//
+// Key concepts demonstrated:
+// - Parameterized theories (Marking depends on PetriNet instance)
+// - Nested instance types (ReachabilityProblem contains Marking instances)
+// - Sort-parameterized theories (Iso takes two sorts as parameters)
+// - Cross-instance references (solution's trace elements reference problem's tokens)
+//
+// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md
+
+// ============================================================
+// THEORY: PetriNet
+// Places, transitions, and arcs with proper arc semantics
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+  in : Sort;     // Input arcs (place -> transition)
+  out : Sort;    // Output arcs (transition -> place)
+
+  in/src : in -> P;    // Input arc source place
+  in/tgt : in -> T;    // Input arc target transition
+  out/src : out -> T;  // Output arc source transition
+  out/tgt : out -> P;  // Output arc target place
+}
+
+// ============================================================
+// THEORY: Marking (parameterized by N : PetriNet)
+// A marking assigns tokens to places
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+// ============================================================
+// THEORY: ReachabilityProblem (parameterized by N : PetriNet)
+// Initial and target markings as nested instances
+// ============================================================
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// ============================================================
+// THEORY: Trace (parameterized by N : PetriNet)
+// A trace records transition firings and token flow via wires
+// ============================================================
+//
+// A trace is a diagrammatic proof of reachability:
+// - Firings represent transition occurrences
+// - Wires connect output arcs of firings to input arcs of other firings
+// - Terminals connect to the initial/target markings
+//
+// The completeness axiom (ax/must_be_fed) ensures every input arc
+// of every firing is accounted for - either wired from another firing
+// or fed by an input terminal.
+
+theory (N : PetriNet instance) Trace {
+  // Firings
+  F : Sort;
+  F/of : F -> N/T;
+
+  // Wires connect output arcs of firings to input arcs of other firings
+  W : Sort;
+  W/src_firing : W -> F;
+  W/src_arc : W -> N/out;
+  W/tgt_firing : W -> F;
+  W/tgt_arc : W -> N/in;
+
+  // Wire coherence: source arc must belong to source firing's transition
+  ax/wire_src_coherent : forall w : W.
+    |- w W/src_arc N/out/src = w W/src_firing F/of;
+
+  // Wire coherence: target arc must belong to target firing's transition
+  ax/wire_tgt_coherent : forall w : W.
+    |- w W/tgt_arc N/in/tgt = w W/tgt_firing F/of;
+
+  // Wire place coherence: wire connects matching places
+  ax/wire_place_coherent : forall w : W.
+    |- w W/src_arc N/out/tgt = w W/tgt_arc N/in/src;
+
+  // Terminals
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+
+  // Terminals connect to specific firings and arcs
+  input_terminal/tgt_firing : input_terminal -> F;
+  input_terminal/tgt_arc : input_terminal -> N/in;
+  output_terminal/src_firing : output_terminal -> F;
+  output_terminal/src_arc : output_terminal -> N/out;
+
+  // Terminal coherence axioms
+  ax/input_terminal_coherent : forall i : input_terminal.
+    |- i input_terminal/tgt_arc N/in/tgt = i input_terminal/tgt_firing F/of;
+
+  ax/output_terminal_coherent : forall o : output_terminal.
+    |- o output_terminal/src_arc N/out/src = o output_terminal/src_firing F/of;
+
+  // Terminal place coherence
+  ax/input_terminal_place : forall i : input_terminal.
+    |- i input_terminal/of = i input_terminal/tgt_arc N/in/src;
+
+  ax/output_terminal_place : forall o : output_terminal.
+    |- o output_terminal/of = o output_terminal/src_arc N/out/tgt;
+
+  // COMPLETENESS: Every arc of every firing must be accounted for.
+
+  // Input completeness: every input arc must be fed by a wire or input terminal
+  ax/input_complete : forall f : F, arc : N/in.
+    arc N/in/tgt = f F/of |-
+    (exists w : W. w W/tgt_firing = f, w W/tgt_arc = arc) \/
+    (exists i : input_terminal. i input_terminal/tgt_firing = f, i input_terminal/tgt_arc = arc);
+
+  // Output completeness: every output arc must be captured by a wire or output terminal
+  ax/output_complete : forall f : F, arc : N/out.
+    arc N/out/src = f F/of |-
+    (exists w : W. w W/src_firing = f, w W/src_arc = arc) \/
+    (exists o : output_terminal. o output_terminal/src_firing = f, o output_terminal/src_arc = arc);
+}
+
+// ============================================================
+// THEORY: Iso (parameterized by two sorts)
+// Isomorphism (bijection) between two sorts
+// ============================================================
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+
+  // Roundtrip axioms ensure this is a true bijection
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+// ============================================================
+// THEORY: Solution (parameterized by N and RP)
+// A constructive witness that target is reachable from initial
+// ============================================================
+
+theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
+  trace : N Trace instance;
+
+  // Bijection: input terminals <-> initial marking tokens
+  initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+
+  // Bijection: output terminals <-> target marking tokens
+  target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
+
+  // Commutativity axioms (currently unchecked):
+  // ax/init_comm : forall i : trace/input_terminal.
+  //   |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of;
+  // ax/target_comm : forall o : trace/output_terminal.
+  //   |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of;
+}
+
+// ============================================================
+// INSTANCE: ExampleNet
+//
+// A Petri net with places A, B, C and transitions:
+//   ab: consumes 1 token from A, produces 1 token in B
+//   ba: consumes 1 token from B, produces 1 token in A
+//   abc: consumes 1 token from A AND 1 from B, produces 1 token in C
+//
+//       +---[ba]----+
+//       v           |
+//      (A) --[ab]->(B) --+
+//       |                |
+//       +----[abc]-------+--> (C)
+//
+// The abc transition is interesting: it requires BOTH an A-token
+// and a B-token to fire, producing a C-token.
+// ============================================================
+
+instance ExampleNet : PetriNet = {
+  A : P; B : P; C : P;
+  ab : T; ba : T; abc : T;
+
+  // A -> B (via ab)
+  ab_in : in;  ab_in in/src = A; ab_in in/tgt = ab;
+  ab_out : out; ab_out out/src = ab; ab_out out/tgt = B;
+
+  // B -> A (via ba)
+  ba_in : in;  ba_in in/src = B; ba_in in/tgt = ba;
+  ba_out : out; ba_out out/src = ba; ba_out out/tgt = A;
+
+  // A + B -> C (via abc) - note: two input arcs!
+  abc_in1 : in; abc_in1 in/src = A; abc_in1 in/tgt = abc;
+  abc_in2 : in; abc_in2 in/src = B; abc_in2 in/tgt = abc;
+  abc_out : out; abc_out out/src = abc; abc_out out/tgt = C;
+}
+
+// ============================================================
+// PROBLEM 0: Can we reach B from A with one token?
+// Initial: 1 token in A
+// Target:  1 token in B
+// ============================================================
+
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    tok : token;
+    tok token/of = ExampleNet/A;
+  };
+  target_marking = {
+    tok : token;
+    tok token/of = ExampleNet/B;
+  };
+}
+
+// ============================================================
+// SOLUTION 0: Yes! Fire transition 'ab' once.
+//
+// This Solution instance is a CONSTRUCTIVE PROOF:
+// - The trace contains one firing (f1) of transition 'ab'
+// - The input terminal feeds the A-token into f1's input arc
+// - The output terminal captures f1's B-token output
+// - The isomorphisms prove the token counts match exactly
+// ============================================================
+
+instance solution0 : ExampleNet problem0 Solution = {
+  trace = {
+    // One firing of transition 'ab'
+    f1 : F;
+    f1 F/of = ExampleNet/ab;
+
+    // Input terminal: feeds the initial A-token into f1
+    it : input_terminal;
+    it input_terminal/of = ExampleNet/A;
+    it input_terminal/tgt_firing = f1;
+    it input_terminal/tgt_arc = ExampleNet/ab_in;
+
+    // Output terminal: captures f1's B-token output
+    ot : output_terminal;
+    ot output_terminal/of = ExampleNet/B;
+    ot output_terminal/src_firing = f1;
+    ot output_terminal/src_arc = ExampleNet/ab_out;
+  };
+
+  initial_iso = {
+    trace/it fwd = problem0/initial_marking/tok;
+    problem0/initial_marking/tok bwd = trace/it;
+  };
+
+  target_iso = {
+    trace/ot fwd = problem0/target_marking/tok;
+    problem0/target_marking/tok bwd = trace/ot;
+  };
+}
+
+// ============================================================
+// PROBLEM 2: Can we reach C from two A-tokens?
+// Initial: 2 tokens in A
+// Target:  1 token in C
+//
+// This is interesting because the only path to C is via 'abc',
+// which requires tokens in BOTH A and B simultaneously.
+// ============================================================
+
+instance problem2 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    t1 : token; t1 token/of = ExampleNet/A;
+    t2 : token; t2 token/of = ExampleNet/A;
+  };
+  target_marking = {
+    t : token;
+    t token/of = ExampleNet/C;
+  };
+}
+
+// ============================================================
+// SOLUTION 2: Yes! Fire 'ab' then 'abc'.
+//
+// Token flow diagram:
+//
+//   [it1]--A-->[f1: ab]--B--wire-->[f2: abc]--C-->[ot]
+//   [it2]--A-----------------^
+//
+// Step 1: Fire 'ab' to move one token A -> B
+//         - it1 feeds A-token into f1 via ab_in
+//         - f1 produces B-token via ab_out
+// Step 2: Fire 'abc' consuming one A-token and one B-token
+//         - it2 feeds A-token into f2 via abc_in1
+//         - Wire connects f1's ab_out to f2's abc_in2 (the B-input)
+//         - f2 produces C-token via abc_out
+// ============================================================
+
+instance solution2 : ExampleNet problem2 Solution = {
+  trace = {
+    // Two firings
+    f1 : F; f1 F/of = ExampleNet/ab;   // First: A -> B
+    f2 : F; f2 F/of = ExampleNet/abc;  // Second: A + B -> C
+
+    // Wire connecting f1's B-output to f2's B-input
+    // This is the crucial connection that makes the trace valid!
+    w1 : W;
+    w1 W/src_firing = f1;
+    w1 W/src_arc = ExampleNet/ab_out;
+    w1 W/tgt_firing = f2;
+    w1 W/tgt_arc = ExampleNet/abc_in2;
+
+    // Input terminal 1: feeds first A-token into f1
+    it1 : input_terminal;
+    it1 input_terminal/of = ExampleNet/A;
+    it1 input_terminal/tgt_firing = f1;
+    it1 input_terminal/tgt_arc = ExampleNet/ab_in;
+
+    // Input terminal 2: feeds second A-token into f2
+    it2 : input_terminal;
+    it2 input_terminal/of = ExampleNet/A;
+    it2 input_terminal/tgt_firing = f2;
+    it2 input_terminal/tgt_arc = ExampleNet/abc_in1;
+
+    // Output terminal: captures f2's C-token output
+    ot : output_terminal;
+    ot output_terminal/of = ExampleNet/C;
+    ot output_terminal/src_firing = f2;
+    ot output_terminal/src_arc = ExampleNet/abc_out;
+  };
+
+  // Bijection: 2 input terminals <-> 2 initial tokens
+  initial_iso = {
+    trace/it1 fwd = problem2/initial_marking/t1;
+    trace/it2 fwd = problem2/initial_marking/t2;
+    problem2/initial_marking/t1 bwd = trace/it1;
+    problem2/initial_marking/t2 bwd = trace/it2;
+  };
+
+  // Bijection: 1 output terminal <-> 1 target token
+  target_iso = {
+    trace/ot fwd = problem2/target_marking/t;
+    problem2/target_marking/t bwd = trace/ot;
+  };
+}

examples/geolog/petri_net_solution.geolog

@@ -0,0 +1,188 @@
+// Full Petri Net Reachability with Synthesized Solution
+//
+// This file contains the complete type-theoretic encoding of Petri net
+// reachability, plus a manually synthesized solution proving that place B
+// is reachable from place A in the example net.
+//
+// ============================================================
+// This instance was synthesized automatically by Claude Opus 4.5.
+// As was this entire file, and this entire project, really.
+// ============================================================
+
+// ============================================================
+// THEORY: PetriNet - Basic structure with arc semantics
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+  in : Sort;     // Input arcs (place -> transition)
+  out : Sort;    // Output arcs (transition -> place)
+
+  in/src : in -> P;    // Input arc source place
+  in/tgt : in -> T;    // Input arc target transition
+  out/src : out -> T;  // Output arc source transition
+  out/tgt : out -> P;  // Output arc target place
+}
+
+// ============================================================
+// THEORY: Marking - Tokens parameterized by a net
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;  // Which place each token is in
+}
+
+// ============================================================
+// THEORY: ReachabilityProblem - Initial and target markings
+// ============================================================
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// ============================================================
+// THEORY: Trace - A sequence of transition firings with wires
+// ============================================================
+//
+// Simplified version for now - full version with product types commented out below.
+
+theory (N : PetriNet instance) Trace {
+  F : Sort;                                    // Firings
+  F/of : F -> N/T;                             // Which transition each fires
+
+  // Terminals for initial/final marking tokens
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+}
+
+// Full Trace theory with wires and product types (not yet fully supported):
+//
+// theory (N : PetriNet instance) Trace {
+//   F : Sort;                                    // Firings
+//   F/of : F -> N/T;                             // Which transition each fires
+//
+//   W : Sort;                                    // Wires connecting firings
+//   W/src : W -> [firing : F, arc : N/out];      // Wire source
+//   W/tgt : W -> [firing : F, arc : N/in];       // Wire target
+//
+//   // Wire coherence axioms
+//   ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of;
+//   ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of;
+//
+//   // Wire uniqueness
+//   ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+//   ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2;
+//
+//   // Terminals for initial/final marking tokens
+//   input_terminal : Sort;
+//   output_terminal : Sort;
+//   input_terminal/of : input_terminal -> N/P;
+//   output_terminal/of : output_terminal -> N/P;
+//   input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+//   output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+//
+//   // Coverage axioms
+//   ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |-
+//     (exists w : W. w W/src = [firing: f, arc: arc]) \/
+//     (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+//   ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |-
+//     (exists w : W. w W/tgt = [firing: f, arc: arc]) \/
+//     (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]);
+// }
+
+// ============================================================
+// THEORY: Iso - Isomorphism between two sorts
+// ============================================================
+
+theory (X : Sort) (Y : Sort) Iso {
+  fwd : X -> Y;
+  bwd : Y -> X;
+  fb : forall x : X. |- x fwd bwd = x;
+  bf : forall y : Y. |- y bwd fwd = y;
+}
+
+// ============================================================
+// THEORY: Solution - A complete reachability witness
+// ============================================================
+
+theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
+  trace : N Trace instance;
+
+  initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
+  target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
+
+  ax/init_comm : forall i : trace/input_terminal.
+    |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of;
+  ax/target_comm : forall o : trace/output_terminal.
+    |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of;
+}
+
+// ============================================================
+// INSTANCE: ExampleNet - A small Petri net
+//
+//   (A) --[ab]--> (B) --[bc]--> (C)
+//    ^             |
+//    +---[ba]------+
+// ============================================================
+
+instance ExampleNet : PetriNet = {
+  A : P; B : P; C : P;
+  ab : T; ba : T; bc : T;
+
+  ab_in : in;  ab_in in/src = A; ab_in in/tgt = ab;
+  ab_out : out; ab_out out/src = ab; ab_out out/tgt = B;
+
+  ba_in : in;  ba_in in/src = B; ba_in in/tgt = ba;
+  ba_out : out; ba_out out/src = ba; ba_out out/tgt = A;
+
+  bc_in : in;  bc_in in/src = B; bc_in in/tgt = bc;
+  bc_out : out; bc_out out/src = bc; bc_out out/tgt = C;
+}
+
+// ============================================================
+// INSTANCE: problem0 - Can we reach B from A?
+// ============================================================
+
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    tok : token;
+    tok token/of = ExampleNet/A;
+  };
+  target_marking = {
+    tok : token;
+    tok token/of = ExampleNet/B;
+  };
+}
+
+// ============================================================
+// INSTANCE: solution0 - YES! Here's the proof.
+// ============================================================
+// This instance was synthesized automatically by Claude Opus 4.5.
+// ============================================================
+
+// The solution proves that place B is reachable from place A by firing
+// transition ab. This creates a trace with one firing and the necessary
+// input/output terminal mappings.
+
+instance solution0 : ExampleNet problem0 Solution = {
+  trace = {
+    f1 : F;
+    f1 F/of = ExampleNet/ab;
+
+    it : input_terminal;
+    it input_terminal/of = ExampleNet/A;
+
+    ot : output_terminal;
+    ot output_terminal/of = ExampleNet/B;
+  };
+
+  // NOTE: Cross-instance references (e.g., trace/it in initial_iso)
+  // are not yet fully supported. The iso instances would map:
+  // - trace/it <-> problem0/initial_marking/tok
+  // - trace/ot <-> problem0/target_marking/tok
+}

examples/geolog/petri_reachability.geolog

@@ -0,0 +1,164 @@
+// Petri Net Reachability - Full Example
+//
+// This demonstrates the core ideas from the original geolog design document:
+// modeling Petri net reachability using geometric logic with the chase algorithm.
+//
+// Original design: loose_thoughts/2025-12-12_12:10.md
+//
+// Key concepts:
+// - PetriNet: places, transitions, input/output arcs
+// - Marking: assignment of tokens to places (parameterized theory)
+// - Trace: sequence of transition firings connecting markings
+// - Reachability: computed via chase algorithm
+
+// ============================================================
+// THEORY: PetriNet
+// ============================================================
+
+theory PetriNet {
+  P : Sort;      // Places
+  T : Sort;      // Transitions
+  In : Sort;     // Input arcs (place -> transition)
+  Out : Sort;    // Output arcs (transition -> place)
+
+  // Arc structure
+  in/place : In -> P;
+  in/trans : In -> T;
+  out/trans : Out -> T;
+  out/place : Out -> P;
+}
+
+// ============================================================
+// THEORY: Marking (parameterized)
+// A marking assigns tokens to places in a specific net
+// ============================================================
+
+theory (N : PetriNet instance) Marking {
+  Token : Sort;
+  of : Token -> N/P;
+}
+
+// ============================================================
+// THEORY: PlaceReachability
+// Simplified reachability at the place level
+// ============================================================
+
+theory PlaceReachability {
+  P : Sort;
+  T : Sort;
+
+  // Which transition connects which places
+  // Fires(t, from, to) means transition t can move a token from 'from' to 'to'
+  Fires : [trans: T, from: P, to: P] -> Prop;
+
+  // Reachability relation (transitive closure)
+  CanReach : [from: P, to: P] -> Prop;
+
+  // Reflexivity: every place can reach itself
+  ax/refl : forall p : P.
+    |- [from: p, to: p] CanReach;
+
+  // Transition firing creates reachability
+  ax/fire : forall t : T, x : P, y : P.
+    [trans: t, from: x, to: y] Fires |- [from: x, to: y] CanReach;
+
+  // Transitivity: reachability composes
+  ax/trans : forall x : P, y : P, z : P.
+    [from: x, to: y] CanReach, [from: y, to: z] CanReach |- [from: x, to: z] CanReach;
+}
+
+// ============================================================
+// INSTANCE: SimpleNet
+// A -> B -> C with bidirectional A <-> B
+//
+//   (A) <--[ba]-- (B) --[bc]--> (C)
+//    |             ^
+//    +---[ab]------+
+// ============================================================
+
+// Uses chase to derive CanReach from axioms (reflexivity, fire, transitivity)
+instance SimpleNet : PlaceReachability = chase {
+  // Places
+  A : P;
+  B : P;
+  C : P;
+
+  // Transitions
+  ab : T;   // A -> B
+  ba : T;   // B -> A
+  bc : T;   // B -> C
+
+  // Firing relations
+  [trans: ab, from: A, to: B] Fires;
+  [trans: ba, from: B, to: A] Fires;
+  [trans: bc, from: B, to: C] Fires;
+}
+
+// ============================================================
+// INSTANCE: MutexNet
+// Two processes competing for a mutex
+//
+//   idle1 --[enter1]--> crit1 --[exit1]--> idle1
+//              ^                    |
+//              |       mutex        |
+//              |                    v
+//   idle2 --[enter2]--> crit2 --[exit2]--> idle2
+// ============================================================
+
+// Uses chase to derive reachability relation
+instance MutexNet : PlaceReachability = chase {
+  // Places
+  idle1 : P;
+  crit1 : P;
+  idle2 : P;
+  crit2 : P;
+  mutex : P;
+
+  // Transitions
+  enter1 : T;
+  exit1 : T;
+  enter2 : T;
+  exit2 : T;
+
+  // Process 1 acquires mutex: idle1 + mutex -> crit1
+  // (simplified: we track place-level, not token-level)
+  [trans: enter1, from: idle1, to: crit1] Fires;
+  [trans: enter1, from: mutex, to: crit1] Fires;
+
+  // Process 1 releases mutex: crit1 -> idle1 + mutex
+  [trans: exit1, from: crit1, to: idle1] Fires;
+  [trans: exit1, from: crit1, to: mutex] Fires;
+
+  // Process 2 acquires mutex: idle2 + mutex -> crit2
+  [trans: enter2, from: idle2, to: crit2] Fires;
+  [trans: enter2, from: mutex, to: crit2] Fires;
+
+  // Process 2 releases mutex: crit2 -> idle2 + mutex
+  [trans: exit2, from: crit2, to: idle2] Fires;
+  [trans: exit2, from: crit2, to: mutex] Fires;
+}
+
+// ============================================================
+// INSTANCE: ProducerConsumerNet
+// Producer creates items, consumer processes them
+//
+//   ready --[produce]--> buffer --[consume]--> done
+// ============================================================
+
+// Uses chase to derive reachability relation
+instance ProducerConsumerNet : PlaceReachability = chase {
+  // Places
+  ready : P;
+  buffer : P;
+  done : P;
+
+  // Transitions
+  produce : T;
+  consume : T;
+
+  // Produce: ready -> buffer
+  [trans: produce, from: ready, to: buffer] Fires;
+
+  // Consume: buffer -> done
+  [trans: consume, from: buffer, to: done] Fires;
+}

examples/geolog/petri_reachability_full_vision.geolog

@@ -0,0 +1,72 @@
+// Full Petri Net Reachability Vision Test
+// From 2025-12-12_12:10_VanillaPetriNetRechability.md
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// Simplified Trace theory without disjunctions for now
+theory (N : PetriNet instance) SimpleTrace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Simplified ax5: every firing+arc gets an output terminal
+  ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc];
+
+  // Simplified ax6: every firing+arc gets an input terminal
+  ax6 : forall f : F, arc : N/in. |- exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc];
+}
+
+instance ExampleNet : PetriNet = {
+  A : P;
+  B : P;
+  ab : T;
+  ab_in : in;
+  ab_in in/src = A;
+  ab_in in/tgt = ab;
+  ab_out : out;
+  ab_out out/src = ab;
+  ab_out out/tgt = B;
+}
+
+// Test nested instance elaboration
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    tok : token;
+    tok token/of = ExampleNet/A;
+  };
+  target_marking = {
+    tok : token;
+    tok token/of = ExampleNet/B;
+  };
+}
+
+// Test chase with SimpleTrace
+instance trace0 : ExampleNet SimpleTrace = chase {
+  f1 : F;
+  f1 F/of = ExampleNet/ab;
+}

examples/geolog/petri_reachability_vision.geolog

@@ -0,0 +1,94 @@
+// Petri Net Reachability Vision Test
+// Based on 2025-12-12 design document
+
+// Basic Petri net structure
+theory PetriNet {
+  // Places
+  P : Sort;
+
+  // Transitions
+  T : Sort;
+
+  // Arcs (input to transitions, output from transitions)
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+// A marking is a multiset of tokens, each at a place
+theory (N : PetriNet instance) Marking {
+  token : Sort;
+  token/of : token -> N/P;
+}
+
+// A reachability problem is: can we get from initial marking to target?
+theory (N : PetriNet instance) ReachabilityProblem {
+  initial_marking : N Marking instance;
+  target_marking : N Marking instance;
+}
+
+// A trace is a sequence of firings connected by wires
+theory (N : PetriNet instance) Trace {
+  // Firings of transitions
+  F : Sort;
+  F/of : F -> N/T;
+
+  // Wires connect firing outputs to firing inputs
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  // Terminals are unconnected arc endpoints (to/from the initial/target markings)
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+}
+
+// Example Petri net: A <--ab/ba--> B, (A,B) --abc--> C
+instance ExampleNet : PetriNet = {
+  A : P;
+  B : P;
+  C : P;
+  ab : T;
+  ba : T;
+  abc : T;
+  ab_in : in;
+  ab_in in/src = A;
+  ab_in in/tgt = ab;
+  ab_out : out;
+  ab_out out/src = ab;
+  ab_out out/tgt = B;
+  ba_in : in;
+  ba_in in/src = B;
+  ba_in in/tgt = ba;
+  ba_out : out;
+  ba_out out/src = ba;
+  ba_out out/tgt = A;
+  abc_in1 : in;
+  abc_in1 in/src = A;
+  abc_in1 in/tgt = abc;
+  abc_in2 : in;
+  abc_in2 in/src = B;
+  abc_in2 in/tgt = abc;
+  abc_out : out;
+  abc_out out/src = abc;
+  abc_out out/tgt = C;
+}
+
+// Reachability problem: Can we reach B from A?
+instance problem0 : ExampleNet ReachabilityProblem = {
+  initial_marking = {
+    t : token;
+    t token/of = ExampleNet/A;
+  };
+  target_marking = {
+    t : token;
+    t token/of = ExampleNet/B;
+  };
+}

examples/geolog/petri_trace_axioms.geolog

@@ -0,0 +1,66 @@
+// Test Trace theory with axioms using product codomains
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+// Trace theory with axioms
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Axiom: wires are injective on source
+  // forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+  // (Commented out - requires product codomain equality in premises)
+
+  // Axiom: every arc endpoint must be wired or terminated
+  // forall f : F, arc : N/out. arc N/out/src = f F/of |-
+  //   (exists w : W. w W/src = [firing: f, arc: arc]) \/
+  //   (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+  // (Commented out - requires product codomain values in conclusions)
+}
+
+// Simple net for testing
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_in : in;
+  arc_in in/src = A;
+  arc_in in/tgt = t;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Test that the basic theory without axioms still works
+instance SimpleTrace : SimpleNet Trace = {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+
+  it : input_terminal;
+  it input_terminal/of = SimpleNet/A;
+  it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in];
+
+  ot : output_terminal;
+  ot output_terminal/of = SimpleNet/B;
+  ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
+}

examples/geolog/petri_trace_coverage_test.geolog

@@ -0,0 +1,36 @@
+// Test: Trace coverage axiom (simplified)
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  out : Sort;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  output_terminal : Sort;
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Simplified ax5: for every arc and firing, if the arc's source is the firing's transition,
+  // create an output terminal
+  ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc];
+}
+
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Trace with just a firing - chase should create a terminal
+instance TestTrace : SimpleNet Trace = chase {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+}

examples/geolog/petri_trace_full_vision.geolog

@@ -0,0 +1,57 @@
+// Trace theory with wires and disjunctions
+// Testing the full vision from 2025-12-12
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+
+  // Every out arc of every firing: either wired or terminal
+  ax5 : forall f : F, arc : N/out. |-
+    (exists w : W. w W/src = [firing: f, arc: arc]) \/
+    (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]);
+
+  // Every in arc of every firing: either wired or terminal
+  ax6 : forall f : F, arc : N/in. |-
+    (exists w : W. w W/tgt = [firing: f, arc: arc]) \/
+    (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]);
+}
+
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_in : in;
+  arc_in in/src = A;
+  arc_in in/tgt = t;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Chase should create both wires AND terminals (naive chase adds all disjuncts)
+instance trace_test : SimpleNet Trace = chase {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+}

examples/geolog/petri_trace_test.geolog

@@ -0,0 +1,58 @@
+// Test that Trace theory with product codomains works
+
+theory PetriNet {
+  P : Sort;
+  T : Sort;
+  in : Sort;
+  out : Sort;
+  in/src : in -> P;
+  in/tgt : in -> T;
+  out/src : out -> T;
+  out/tgt : out -> P;
+}
+
+// Simple Petri net: A --t--> B
+instance SimpleNet : PetriNet = {
+  A : P;
+  B : P;
+  t : T;
+  arc_in : in;
+  arc_in in/src = A;
+  arc_in in/tgt = t;
+  arc_out : out;
+  arc_out out/src = t;
+  arc_out out/tgt = B;
+}
+
+// Trace theory with product codomains for wire endpoints
+theory (N : PetriNet instance) Trace {
+  F : Sort;
+  F/of : F -> N/T;
+
+  W : Sort;
+  W/src : W -> [firing : F, arc : N/out];
+  W/tgt : W -> [firing : F, arc : N/in];
+
+  input_terminal : Sort;
+  output_terminal : Sort;
+  input_terminal/of : input_terminal -> N/P;
+  output_terminal/of : output_terminal -> N/P;
+  input_terminal/tgt : input_terminal -> [firing : F, arc : N/in];
+  output_terminal/src : output_terminal -> [firing : F, arc : N/out];
+}
+
+// A simple trace: one firing of t, with input/output terminals
+instance SimpleTrace : SimpleNet Trace = {
+  f1 : F;
+  f1 F/of = SimpleNet/t;
+
+  // Input terminal (token comes from external marking)
+  it : input_terminal;
+  it input_terminal/of = SimpleNet/A;
+  it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in];
+
+  // Output terminal (token goes to external marking)
+  ot : output_terminal;
+  ot output_terminal/of = SimpleNet/B;
+  ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out];
+}

examples/geolog/preorder.geolog

@@ -0,0 +1,42 @@
+// Preorder: a set with a reflexive, transitive relation
+//
+// This demonstrates RELATIONS (predicates) as opposed to functions.
+// A relation R : A -> Prop is a predicate on A.
+// For binary relations, we use a product domain: R : [x: A, y: A] -> Prop
+
+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 ∧ y ≤ z → 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;
+}
+
+// The discrete preorder: only reflexive pairs
+// (no elements are comparable except to themselves)
+// Uses `chase` to automatically derive reflexive pairs from axiom ax/refl.
+instance Discrete3 : Preorder = chase {
+  a : X;
+  b : X;
+  c : X;
+}
+
+// A total order on 3 elements: a ≤ b ≤ c
+// Uses `chase` to derive reflexive and transitive closure.
+instance Chain3 : Preorder = chase {
+  bot : X;
+  mid : X;
+  top : X;
+
+  // Assert the basic ordering; chase will add reflexive pairs
+  // and transitive closure (bot ≤ top)
+  [x: bot, y: mid] leq;
+  [x: mid, y: top] leq;
+}

examples/geolog/product_codomain_equality_test.geolog

@@ -0,0 +1,23 @@
+// Test: Product codomain equality in premise (ax3 pattern)
+
+theory ProductCodomainEqTest {
+  A : Sort;
+  B : Sort;
+
+  W : Sort;
+  W/src : W -> [x: A, y: B];
+
+  // ax3 pattern: forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2
+  // This should make W injective on src
+  ax_inj : forall w1 : W, w2 : W. w1 W/src = w2 W/src |- w1 = w2;
+}
+
+// Instance with two wires that have the same src - should be identified by chase
+instance Test : ProductCodomainEqTest = {
+  a1 : A;
+  b1 : B;
+  w1 : W;
+  w1 W/src = [x: a1, y: b1];
+  w2 : W;
+  w2 W/src = [x: a1, y: b1];
+}

examples/geolog/product_codomain_test.geolog

@@ -0,0 +1,51 @@
+// Test: Product Codomain Support
+//
+// This tests the new feature where functions can have product codomains,
+// allowing record literal assignments like:
+//   elem func = [field1: v1, field2: v2];
+
+theory ProductCodomainTest {
+  A : Sort;
+  B : Sort;
+  C : Sort;
+
+  // Function with product codomain: maps A elements to (B, C) pairs
+  pair_of : A -> [left: B, right: C];
+}
+
+instance TestInstance : ProductCodomainTest = {
+  // Elements
+  a1 : A;
+  b1 : B;
+  b2 : B;
+  c1 : C;
+
+  // Assign product codomain value using record literal
+  a1 pair_of = [left: b1, right: c1];
+}
+
+// A more realistic example: Edges in a graph
+theory DirectedGraph {
+  V : Sort;
+  E : Sort;
+
+  // Edge endpoints as a product codomain
+  endpoints : E -> [src: V, tgt: V];
+}
+
+instance TriangleGraph : DirectedGraph = {
+  // Vertices
+  v0 : V;
+  v1 : V;
+  v2 : V;
+
+  // Edges
+  e01 : E;
+  e12 : E;
+  e20 : E;
+
+  // Assign edge endpoints using record literals
+  e01 endpoints = [src: v0, tgt: v1];
+  e12 endpoints = [src: v1, tgt: v2];
+  e20 endpoints = [src: v2, tgt: v0];
+}

examples/geolog/record_existential_test.geolog

@@ -0,0 +1,18 @@
+// Test: Record literals in existential conclusions
+
+theory RecordExistentialTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Axiom: given any a:A and b:B, there exists an R with that data
+  ax1 : forall a : A, b : B. |-
+    exists r : R. r R/data = [x: a, y: b];
+}
+
+instance Test : RecordExistentialTest = chase {
+  a1 : A;
+  b1 : B;
+}

examples/geolog/record_in_axiom_test.geolog

@@ -0,0 +1,12 @@
+// Test: Record literals in axioms
+
+theory RecordAxiomTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Test axiom with record literal RHS
+  ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- true;
+}

examples/geolog/record_premise_chase_test.geolog

@@ -0,0 +1,23 @@
+// Test: Chase with record literals in premises
+
+theory RecordPremiseTest {
+  A : Sort;
+  B : Sort;
+
+  R : Sort;
+  R/data : R -> [x: A, y: B];
+
+  // Derived sort for processed items
+  Processed : Sort;
+  Processed/r : Processed -> R;
+
+  // Axiom: given r with data [x: a, y: b], create a Processed for it
+  ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists p : Processed. p Processed/r = r;
+}
+
+instance Test : RecordPremiseTest = {
+  a1 : A;
+  b1 : B;
+  r1 : R;
+  r1 R/data = [x: a1, y: b1];
+}

examples/geolog/relalg_simple.geolog

@@ -0,0 +1,130 @@
+// Example: RelAlgIR query plan instances
+//
+// This demonstrates creating query plans as RelAlgIR instances.
+// These show the string diagram representation of relational algebra.
+//
+// First we need to load both GeologMeta (for Srt, Func, etc.) and RelAlgIR.
+// This file just defines instances; load theories first in the REPL:
+//   :load theories/GeologMeta.geolog
+//   :load theories/RelAlgIR.geolog
+//   :load examples/geolog/relalg_simple.geolog
+//
+// Note: RelAlgIR extends GeologMeta, so a RelAlgIR instance contains
+// elements from both GeologMeta sorts (Srt, Func, Elem) and RelAlgIR
+// sorts (Wire, Schema, ScanOp, etc.)
+
+// ============================================================
+// Example 1: Simple Scan
+// ============================================================
+// Query: "scan all elements of sort V"
+// Plan:  () --[ScanOp]--> Wire
+
+instance ScanV : RelAlgIR = chase {
+  // -- Schema (target theory) --
+  target_theory : GeologMeta/Theory;
+  target_theory GeologMeta/Theory/parent = target_theory;
+
+  v_srt : GeologMeta/Srt;
+  v_srt GeologMeta/Srt/theory = target_theory;
+
+  // -- Query Plan --
+  v_base_schema : BaseSchema;
+  v_base_schema BaseSchema/srt = v_srt;
+
+  v_schema : Schema;
+  v_base_schema BaseSchema/schema = v_schema;
+
+  scan_out : Wire;
+  scan_out Wire/schema = v_schema;
+
+  scan : ScanOp;
+  scan ScanOp/srt = v_srt;
+  scan ScanOp/out = scan_out;
+
+  scan_op : Op;
+  scan ScanOp/op = scan_op;
+}
+
+// ============================================================
+// Example 2: Filter(Scan)
+// ============================================================
+// Query: "scan E, filter where src(e) = some vertex"
+// Plan:  () --[Scan]--> w1 --[Filter]--> w2
+//
+// This demonstrates composition via wire sharing.
+
+// Uses chase to derive relations.
+instance FilterScan : RelAlgIR = chase {
+  // -- Schema (representing Graph theory) --
+  target_theory : GeologMeta/Theory;
+  target_theory GeologMeta/Theory/parent = target_theory;
+
+  // Sorts: V (vertices), E (edges)
+  v_srt : GeologMeta/Srt;
+  v_srt GeologMeta/Srt/theory = target_theory;
+
+  e_srt : GeologMeta/Srt;
+  e_srt GeologMeta/Srt/theory = target_theory;
+
+  // Functions: src : E -> V
+  // First create the DSort wrappers
+  v_base_ds : GeologMeta/BaseDS;
+  v_base_ds GeologMeta/BaseDS/srt = v_srt;
+
+  e_base_ds : GeologMeta/BaseDS;
+  e_base_ds GeologMeta/BaseDS/srt = e_srt;
+
+  v_dsort : GeologMeta/DSort;
+  v_base_ds GeologMeta/BaseDS/dsort = v_dsort;
+
+  e_dsort : GeologMeta/DSort;
+  e_base_ds GeologMeta/BaseDS/dsort = e_dsort;
+
+  src_func : GeologMeta/Func;
+  src_func GeologMeta/Func/theory = target_theory;
+  src_func GeologMeta/Func/dom = e_dsort;
+  src_func GeologMeta/Func/cod = v_dsort;
+
+  // NOTE: For a complete example, we'd also need an Instance element
+  // and Elem elements. For simplicity, we use a simpler predicate structure.
+
+  // Using TruePred for now (matches all, demonstrating structure)
+
+  // -- Query Plan --
+  // Schema for E
+  e_base_schema : BaseSchema;
+  e_base_schema BaseSchema/srt = e_srt;
+
+  e_schema : Schema;
+  e_base_schema BaseSchema/schema = e_schema;
+
+  // Wire 1: output of Scan (E elements)
+  w1 : Wire;
+  w1 Wire/schema = e_schema;
+
+  // Wire 2: output of Filter (filtered E elements)
+  w2 : Wire;
+  w2 Wire/schema = e_schema;
+
+  // Scan operation
+  scan : ScanOp;
+  scan ScanOp/srt = e_srt;
+  scan ScanOp/out = w1;
+
+  scan_op : Op;
+  scan ScanOp/op = scan_op;
+
+  // Predicate: TruePred (matches all - demonstrates filter structure)
+  true_pred : TruePred;
+  pred_elem : Pred;
+  true_pred TruePred/pred = pred_elem;
+
+  // Filter operation: w1 --[Filter(pred)]--> w2
+  filter : FilterOp;
+  filter FilterOp/in = w1;
+  filter FilterOp/out = w2;
+  filter FilterOp/pred = pred_elem;
+
+  filter_op : Op;
+  filter FilterOp/op = filter_op;
+}

examples/geolog/solver_demo.geolog

@@ -0,0 +1,132 @@
+// Solver Demo: Theories demonstrating the geometric logic solver
+//
+// Use the :solve command to find instances of these theories:
+//   :source examples/geolog/solver_demo.geolog
+//   :solve EmptyModel
+//   :solve Inhabited
+//   :solve Inconsistent
+//
+// The solver uses forward chaining to automatically:
+// - Add witness elements for existentials
+// - Assert relation tuples
+// - Detect unsatisfiability (derivation of False)
+
+// ============================================================================
+// Theory 1: EmptyModel - Trivially satisfiable with empty carrier
+// ============================================================================
+//
+// A theory with no axioms is satisfied by the empty structure.
+// The solver should report SOLVED immediately with 0 elements.
+
+theory EmptyModel {
+  A : Sort;
+  B : Sort;
+  f : A -> B;
+  R : A -> Prop;
+}
+
+// ============================================================================
+// Theory 2: UnconditionalExistential - Requires witness creation
+// ============================================================================
+//
+// Axiom: forall x : P. |- exists y : P. y R
+//
+// SUBTLE: This axiom's premise (True) and conclusion (∃y.R(y)) don't mention x!
+// So even though there's a "forall x : P", the check happens once for an empty
+// assignment. The premise True holds, but ∃y.R(y) doesn't hold for empty P
+// (no witnesses). The solver correctly detects this and adds a witness.
+//
+// This is correct geometric logic semantics! The universal over x doesn't
+// protect against empty P because x isn't used in the formulas.
+
+theory UnconditionalExistential {
+  P : Sort;
+  R : P -> Prop;
+
+  // This effectively says "there must exist some y with R(y)"
+  // because x is unused - the check happens once regardless of |P|
+  ax : forall x : P. |- exists y : P. y R;
+}
+
+// ============================================================================
+// Theory 3: VacuouslyTrue - Axiom that IS vacuously true for empty carriers
+// ============================================================================
+//
+// Axiom: forall x : P. |- x R
+//
+// For every x, assert R(x). When P is empty, there are no x values to check,
+// so the axiom is vacuously satisfied. Compare with UnconditionalExistential!
+
+theory VacuouslyTrue {
+  P : Sort;
+  R : P -> Prop;
+
+  // This truly IS vacuously true for empty P because x IS used in the conclusion
+  ax : forall x : P. |- x R;
+}
+
+// ============================================================================
+// Theory 4: Inconsistent - UNSAT via derivation of False
+// ============================================================================
+//
+// Axiom: forall x. |- false
+//
+// For any element x, we derive False. This is immediately UNSAT.
+// The solver detects this and reports UNSAT.
+
+theory Inconsistent {
+  A : Sort;
+
+  // Contradiction: any element leads to False
+  ax : forall a : A. |- false;
+}
+
+// ============================================================================
+// Theory 5: ReflexiveRelation - Forward chaining asserts reflexive tuples
+// ============================================================================
+//
+// Axiom: forall x. |- R(x, x)
+//
+// For every element x, the pair (x, x) is in relation R.
+// The solver will assert R(x, x) for each element added.
+
+theory ReflexiveRelation {
+  X : Sort;
+  R : [a: X, b: X] -> Prop;
+
+  // Reflexivity: every element is related to itself
+  ax/refl : forall x : X. |- [a: x, b: x] R;
+}
+
+// ============================================================================
+// Theory 6: ChainedWitness - Nested existential body processing
+// ============================================================================
+//
+// Axiom: forall x. |- exists y. exists z. E(x, y), E(y, z)
+//
+// For every x, there exist y and z such that E(x,y) and E(y,z).
+// Forward chaining creates witnesses and asserts the relations.
+
+theory ChainedWitness {
+  N : Sort;
+  E : [src: N, tgt: N] -> Prop;
+
+  // Chain: every node has a two-step path out
+  ax/chain : forall x : N. |- exists y : N. exists z : N. [src: x, tgt: y] E, [src: y, tgt: z] E;
+}
+
+// ============================================================================
+// Theory 7: EqualityCollapse - Equation handling via congruence closure
+// ============================================================================
+//
+// Axiom: forall x, y. |- x = y
+//
+// All elements of sort X are equal. The solver adds equations to the
+// congruence closure and merges equivalence classes.
+
+theory EqualityCollapse {
+  X : Sort;
+
+  // All elements are equal
+  ax/all_equal : forall x : X, y : X. |- x = y;
+}

examples/geolog/sort_param_simple.geolog

@@ -0,0 +1,31 @@
+// Simpler sort parameter test
+
+theory (X : Sort) Container {
+  elem : X;  // not a Sort, but an element of X
+}
+
+// Hmm, this doesn't quite work...
+// Let me try the actual vision pattern
+
+theory Base {
+  A : Sort;
+  B : Sort;
+}
+
+instance MyBase : Base = {
+  a1 : A;
+  a2 : A;
+  b1 : B;
+  b2 : B;
+}
+
+// Now try a theory parameterized by an instance
+theory (Inst : Base instance) Map {
+  map : Inst/A -> Inst/B;
+}
+
+// Instance of Map parameterized by MyBase
+instance MyMap : MyBase Map = {
+  a1 map = MyBase/b1;
+  a2 map = MyBase/b2;
+}

examples/geolog/todo_list.geolog

@@ -0,0 +1,44 @@
+// TodoList: A simple relational model for tracking tasks
+//
+// This demonstrates geolog as a persistent relational database.
+// Elements represent tasks, and relations track their status.
+
+theory TodoList {
+  // The sort of todo items
+  Item : Sort;
+
+  // Unary relations for item status (simple arrow syntax)
+  completed : Item -> Prop;
+  high_priority : Item -> Prop;
+  blocked : Item -> Prop;
+
+  // Binary relation for dependencies
+  depends : [item: Item, on: Item] -> Prop;
+
+  // Axiom: if an item depends on another, either it is blocked
+  // or the dependency is completed
+  ax/dep_blocked : forall x : Item, y : Item.
+    [item: x, on: y] depends |- x blocked \/ y completed;
+}
+
+// Example: An empty todo list ready for interactive use
+instance MyTodos : TodoList = {
+  // Start empty - add items interactively with :add
+}
+
+// Example: A pre-populated todo list
+instance SampleTodos : TodoList = {
+  // Items
+  buy_groceries : Item;
+  cook_dinner : Item;
+  do_laundry : Item;
+  clean_house : Item;
+
+  // Status: unary relations use simple syntax
+  buy_groceries completed;
+  cook_dinner high_priority;
+
+  // Dependencies: cook_dinner depends on buy_groceries
+  // Mixed syntax: first positional arg maps to 'item' field
+  [cook_dinner, on: buy_groceries] depends;
+}

examples/geolog/transitive_closure.geolog

@@ -0,0 +1,77 @@
+// Transitive Closure Example
+//
+// This example demonstrates the chase algorithm computing transitive
+// closure of a relation. We define a Graph theory with Edge and Path
+// relations, where Path is the transitive closure of Edge.
+//
+// Run with:
+//   cargo run -- examples/geolog/transitive_closure.geolog
+// Then:
+//   :source examples/geolog/transitive_closure.geolog
+//   :inspect Chain
+//   :chase Chain
+//
+// The chase will derive Path tuples for all reachable pairs:
+// - Edge(a,b), Edge(b,c), Edge(c,d) as base facts
+// - Path(a,b), Path(b,c), Path(c,d) from base axiom
+// - Path(a,c), Path(b,d) from one step of transitivity
+// - Path(a,d) from two steps of transitivity
+
+theory Graph {
+  V : Sort;
+
+  // Direct edges in the graph
+  Edge : [src: V, tgt: V] -> Prop;
+
+  // Reachability (transitive closure of Edge)
+  Path : [src: V, tgt: V] -> Prop;
+
+  // Base case: every edge is a path
+  ax/base : forall x, y : V.
+    [src: x, tgt: y] Edge |- [src: x, tgt: y] Path;
+
+  // Inductive case: paths compose
+  ax/trans : forall x, y, z : V.
+    [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path;
+}
+
+// A linear chain: a -> b -> c -> d
+// Chase derives Path tuples from Edge via ax/base and ax/trans.
+instance Chain : Graph = chase {
+  a : V;
+  b : V;
+  c : V;
+  d : V;
+
+  // Edges form a chain
+  [src: a, tgt: b] Edge;
+  [src: b, tgt: c] Edge;
+  [src: c, tgt: d] Edge;
+}
+
+// A diamond: a -> b, a -> c, b -> d, c -> d
+// Chase derives all reachable paths.
+instance Diamond : Graph = chase {
+  top : V;
+  left : V;
+  right : V;
+  bottom : V;
+
+  // Two paths from top to bottom
+  [src: top, tgt: left] Edge;
+  [src: top, tgt: right] Edge;
+  [src: left, tgt: bottom] Edge;
+  [src: right, tgt: bottom] Edge;
+}
+
+// A cycle: a -> b -> c -> a
+// Chase derives all reachable paths (full connectivity).
+instance Cycle : Graph = chase {
+  x : V;
+  y : V;
+  z : V;
+
+  [src: x, tgt: y] Edge;
+  [src: y, tgt: z] Edge;
+  [src: z, tgt: x] Edge;
+}

examples/scripts/README.md

@@ -0,0 +1,13 @@
+# Example Scripts
+
+These scripts can be executed with:
+
+```bash
+make script SCRIPT=examples/scripts/ancestor.chase
+```
+
+Available examples:
+
+- `ancestor.chase`: transitive closure over `Parent/2`
+- `employee_departments.chase`: existential rule that creates labeled nulls
+- `same_team.chase`: conjunctive query with a self-join

examples/scripts/ancestor.chase

@@ -0,0 +1,11 @@
+# Derive ancestors from parent relationships.
+
+fact Parent(alice, bob).
+fact Parent(bob, carol).
+fact Parent(carol, dave).
+
+rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
+rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z).
+
+run.
+query Ancestor(?X, ?Y)?

examples/scripts/employee_departments.chase

@@ -0,0 +1,11 @@
+# Existential rule example: each employee works in some department.
+
+fact Employee(alice).
+fact Employee(bob).
+fact Employee(carol).
+
+rule Employee(?X) -> WorksIn(?X, ?Dept).
+
+run.
+show facts
+query WorksIn(?X, ?Dept)?

examples/scripts/same_team.chase

@@ -0,0 +1,11 @@
+# Query people who share a manager.
+
+fact ManagedBy(alice, eve).
+fact ManagedBy(bob, eve).
+fact ManagedBy(carol, frank).
+
+rule ManagedBy(?X, ?M), ManagedBy(?Y, ?M) -> SameTeam(?X, ?Y).
+
+run.
+query SameTeam(?X, ?Y)?
+query SameTeam(alice, bob)?

src/catalog/mod.rs

@@ -0,0 +1,133 @@
+//! Minimal catalog support for mapping predicates to relational schemas.
+
+use std::collections::HashMap;
+use std::error::Error;
+use std::fmt;
+
+use crate::chase::{Instance, Term};
+use crate::relational::{DataType, Field, Schema};
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum CatalogError {
+    UnknownTable(String),
+    InconsistentArity {
+        table: String,
+        expected: usize,
+        found: usize,
+    },
+}
+
+impl fmt::Display for CatalogError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::UnknownTable(table) => write!(f, "unknown table `{}`", table),
+            Self::InconsistentArity {
+                table,
+                expected,
+                found,
+            } => write!(
+                f,
+                "table `{}` has inconsistent arity: expected {}, found {}",
+                table, expected, found
+            ),
+        }
+    }
+}
+
+impl Error for CatalogError {}
+
+#[derive(Debug, Clone, Default)]
+pub struct PredicateCatalog {
+    schemas: HashMap<String, Schema>,
+}
+
+impl PredicateCatalog {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn register_table(&mut self, table: impl Into<String>, schema: Schema) {
+        self.schemas.insert(table.into(), schema);
+    }
+
+    pub fn schema_for(&self, table: &str) -> Result<&Schema, CatalogError> {
+        self.schemas
+            .get(table)
+            .ok_or_else(|| CatalogError::UnknownTable(table.to_string()))
+    }
+
+    pub fn from_instance(instance: &Instance) -> Result<Self, CatalogError> {
+        let mut arities = HashMap::new();
+        let mut nullable_positions: HashMap<String, Vec<bool>> = HashMap::new();
+
+        for atom in instance.iter() {
+            let arity = atom.arity();
+            match arities.get(&atom.predicate) {
+                Some(expected) if *expected != arity => {
+                    return Err(CatalogError::InconsistentArity {
+                        table: atom.predicate.clone(),
+                        expected: *expected,
+                        found: arity,
+                    });
+                }
+                Some(_) => {}
+                None => {
+                    arities.insert(atom.predicate.clone(), arity);
+                    nullable_positions.insert(atom.predicate.clone(), vec![false; arity]);
+                }
+            }
+
+            if let Some(positions) = nullable_positions.get_mut(&atom.predicate) {
+                for (index, term) in atom.terms.iter().enumerate() {
+                    if matches!(term, Term::Null(_)) {
+                        positions[index] = true;
+                    }
+                }
+            }
+        }
+
+        let mut catalog = Self::new();
+        for (table, arity) in arities {
+            let nullable = nullable_positions.remove(&table).unwrap_or_default();
+            let fields = (0..arity)
+                .map(|index| {
+                    Field::new(
+                        format!("c{}", index),
+                        DataType::Text,
+                        nullable.get(index).copied().unwrap_or(false),
+                    )
+                })
+                .collect();
+            catalog.register_table(table, Schema::new(fields));
+        }
+
+        Ok(catalog)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::chase::Atom;
+
+    #[test]
+    fn infers_predicate_schemas_from_instance() {
+        let instance: Instance = vec![
+            Atom::new(
+                "Parent",
+                vec![Term::constant("alice"), Term::constant("bob")],
+            ),
+            Atom::new("Parent", vec![Term::constant("bob"), Term::null(0)]),
+        ]
+        .into_iter()
+        .collect();
+
+        let catalog = PredicateCatalog::from_instance(&instance).unwrap();
+        let schema = catalog.schema_for("Parent").unwrap();
+
+        assert_eq!(schema.len(), 2);
+        assert_eq!(schema.fields()[0].name(), "c0");
+        assert_eq!(schema.fields()[1].name(), "c1");
+        assert!(schema.fields()[1].nullable());
+    }
+}

src/execution/mod.rs

@@ -0,0 +1,112 @@
+//! Minimal execution support for the first SQL slice.
+
+use std::error::Error;
+use std::fmt;
+
+use crate::chase::{Instance, Term};
+use crate::planner::logical::{LogicalExpr, LogicalPlan};
+use crate::relational::{ResultSet, Row, Value};
+
+#[derive(Debug)]
+pub enum ExecutionError {
+    UnknownColumn(String),
+    NonGroundScanTerm,
+}
+
+impl fmt::Display for ExecutionError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::UnknownColumn(column) => write!(f, "unknown column `{}`", column),
+            Self::NonGroundScanTerm => {
+                write!(f, "cannot scan non-ground terms into relational rows")
+            }
+        }
+    }
+}
+
+impl Error for ExecutionError {}
+
+pub fn execute(plan: &LogicalPlan, instance: &Instance) -> Result<ResultSet, ExecutionError> {
+    match plan {
+        LogicalPlan::Scan { table, schema } => {
+            let mut rows = Vec::new();
+            for fact in instance.facts_for_predicate(table) {
+                let values = fact
+                    .terms
+                    .iter()
+                    .map(value_from_term)
+                    .collect::<Result<Vec<_>, _>>()?;
+                rows.push(Row::new(values));
+            }
+            Ok(ResultSet::new(schema.clone(), rows))
+        }
+        LogicalPlan::Filter { input, predicate } => {
+            let result = execute(input, instance)?;
+            let filtered_rows = result
+                .rows()
+                .iter()
+                .filter(|row| eval_predicate(predicate, row, result.schema()).unwrap_or(false))
+                .cloned()
+                .collect();
+            Ok(ResultSet::new(result.schema().clone(), filtered_rows))
+        }
+        LogicalPlan::Project {
+            input,
+            expressions,
+            schema,
+        } => {
+            let result = execute(input, instance)?;
+            let mut rows = Vec::new();
+            for row in result.rows() {
+                let values = expressions
+                    .iter()
+                    .map(|expr| eval_expr(&expr.expr, row, result.schema()))
+                    .collect::<Result<Vec<_>, _>>()?;
+                rows.push(Row::new(values));
+            }
+            Ok(ResultSet::new(schema.clone(), rows))
+        }
+    }
+}
+
+fn eval_predicate(
+    expr: &LogicalExpr,
+    row: &Row,
+    schema: &crate::relational::Schema,
+) -> Result<bool, ExecutionError> {
+    match expr {
+        LogicalExpr::Eq(left, right) => Ok(eval_expr(left, row, schema)?
+            .sql_eq(&eval_expr(right, row, schema)?)
+            .unwrap_or(false)),
+        _ => Ok(false),
+    }
+}
+
+fn eval_expr(
+    expr: &LogicalExpr,
+    row: &Row,
+    schema: &crate::relational::Schema,
+) -> Result<Value, ExecutionError> {
+    match expr {
+        LogicalExpr::Column(name) => {
+            let index = schema
+                .index_of(name)
+                .ok_or_else(|| ExecutionError::UnknownColumn(name.clone()))?;
+            Ok(row.get(index).cloned().unwrap_or(Value::Null))
+        }
+        LogicalExpr::Literal(value) => Ok(value.clone()),
+        LogicalExpr::Eq(left, right) => {
+            let left = eval_expr(left, row, schema)?;
+            let right = eval_expr(right, row, schema)?;
+            Ok(Value::Boolean(left.sql_eq(&right).unwrap_or(false)))
+        }
+    }
+}
+
+fn value_from_term(term: &Term) -> Result<Value, ExecutionError> {
+    match term {
+        Term::Constant(value) => Ok(Value::text(value.clone())),
+        Term::Null(_) => Ok(Value::Null),
+        Term::Variable(_) => Err(ExecutionError::NonGroundScanTerm),
+    }
+}

src/lib.rs

@@ -4,8 +4,13 @@
 //! lightweight frontends for experimenting with rule-driven query answering.
 //! It is not yet a full SQL engine with logical and physical planning layers.
 
+pub mod catalog;
 pub mod chase;
+pub mod execution;
 pub mod frontend;
+pub mod planner;
+pub mod relational;
+pub mod sql;
 
 // Curated convenience re-exports for the current public crate surface.
 // Lower-level reasoning and provenance APIs remain under `query_engine::chase`.

src/planner/logical.rs

@@ -0,0 +1,47 @@
+use crate::relational::{ResultSet, Schema, Value};
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum LogicalExpr {
+    Column(String),
+    Literal(Value),
+    Eq(Box<LogicalExpr>, Box<LogicalExpr>),
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct NamedExpr {
+    pub name: String,
+    pub expr: LogicalExpr,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum LogicalPlan {
+    Scan {
+        table: String,
+        schema: Schema,
+    },
+    Filter {
+        input: Box<LogicalPlan>,
+        predicate: LogicalExpr,
+    },
+    Project {
+        input: Box<LogicalPlan>,
+        expressions: Vec<NamedExpr>,
+        schema: Schema,
+    },
+}
+
+impl LogicalPlan {
+    pub fn output_schema(&self) -> &Schema {
+        match self {
+            Self::Scan { schema, .. } => schema,
+            Self::Filter { input, .. } => input.output_schema(),
+            Self::Project { schema, .. } => schema,
+        }
+    }
+}
+
+impl From<ResultSet> for LogicalPlan {
+    fn from(_: ResultSet) -> Self {
+        unreachable!("result sets are execution output, not logical plans")
+    }
+}

src/planner/mod.rs

@@ -0,0 +1,4 @@
+//! Logical planning scaffolding.
+
+pub mod logical;
+pub mod sql;

src/planner/sql.rs

@@ -0,0 +1,149 @@
+use std::error::Error;
+use std::fmt;
+
+use crate::catalog::{CatalogError, PredicateCatalog};
+use crate::planner::logical::{LogicalExpr, LogicalPlan, NamedExpr};
+use crate::relational::{Field, Schema, Value};
+use crate::sql::ast::{BinaryOp, Expr, Literal, Select, SelectItem};
+
+#[derive(Debug)]
+pub enum PlannerError {
+    Catalog(CatalogError),
+    UnknownColumn(String),
+    UnsupportedProjection,
+}
+
+impl fmt::Display for PlannerError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::Catalog(err) => write!(f, "catalog error: {}", err),
+            Self::UnknownColumn(column) => write!(f, "unknown column `{}`", column),
+            Self::UnsupportedProjection => {
+                write!(f, "only wildcard and column projections are supported")
+            }
+        }
+    }
+}
+
+impl Error for PlannerError {
+    fn source(&self) -> Option<&(dyn Error + 'static)> {
+        match self {
+            Self::Catalog(err) => Some(err),
+            Self::UnknownColumn(_) | Self::UnsupportedProjection => None,
+        }
+    }
+}
+
+impl From<CatalogError> for PlannerError {
+    fn from(value: CatalogError) -> Self {
+        Self::Catalog(value)
+    }
+}
+
+pub fn plan_select(
+    select: &Select,
+    catalog: &PredicateCatalog,
+) -> Result<LogicalPlan, PlannerError> {
+    let scan_schema = catalog.schema_for(&select.from)?.clone();
+    let mut plan = LogicalPlan::Scan {
+        table: select.from.clone(),
+        schema: scan_schema.clone(),
+    };
+
+    if let Some(selection) = &select.selection {
+        let predicate = plan_expr(selection, &scan_schema)?;
+        plan = LogicalPlan::Filter {
+            input: Box::new(plan),
+            predicate,
+        };
+    }
+
+    if is_wildcard_projection(&select.projection) {
+        return Ok(plan);
+    }
+
+    let mut expressions = Vec::new();
+    let mut fields = Vec::new();
+    for item in &select.projection {
+        match item {
+            SelectItem::Expr { expr, alias } => match expr {
+                Expr::Identifier(name) => {
+                    let index = scan_schema
+                        .index_of(name)
+                        .ok_or_else(|| PlannerError::UnknownColumn(name.clone()))?;
+                    let input_field = &scan_schema.fields()[index];
+                    let output_name = alias.clone().unwrap_or_else(|| name.clone());
+                    expressions.push(NamedExpr {
+                        name: output_name.clone(),
+                        expr: LogicalExpr::Column(name.clone()),
+                    });
+                    fields.push(Field::new(
+                        output_name,
+                        input_field.data_type().clone(),
+                        input_field.nullable(),
+                    ));
+                }
+                _ => return Err(PlannerError::UnsupportedProjection),
+            },
+            SelectItem::Wildcard => return Err(PlannerError::UnsupportedProjection),
+        }
+    }
+
+    Ok(LogicalPlan::Project {
+        input: Box::new(plan),
+        expressions,
+        schema: Schema::new(fields),
+    })
+}
+
+fn is_wildcard_projection(items: &[SelectItem]) -> bool {
+    matches!(items, [SelectItem::Wildcard])
+}
+
+fn plan_expr(expr: &Expr, schema: &Schema) -> Result<LogicalExpr, PlannerError> {
+    match expr {
+        Expr::Identifier(name) => {
+            if schema.index_of(name).is_none() {
+                return Err(PlannerError::UnknownColumn(name.clone()));
+            }
+            Ok(LogicalExpr::Column(name.clone()))
+        }
+        Expr::Literal(literal) => Ok(LogicalExpr::Literal(plan_literal(literal))),
+        Expr::Binary { left, op, right } => match op {
+            BinaryOp::Eq => Ok(LogicalExpr::Eq(
+                Box::new(plan_expr(left, schema)?),
+                Box::new(plan_expr(right, schema)?),
+            )),
+        },
+    }
+}
+
+fn plan_literal(literal: &Literal) -> Value {
+    match literal {
+        Literal::String(value) => Value::text(value.clone()),
+        Literal::Null => Value::Null,
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::catalog::PredicateCatalog;
+    use crate::chase::{Atom, Instance, Term};
+    use crate::sql::parser::parse_select;
+
+    #[test]
+    fn plans_projection_and_filter() {
+        let instance: Instance = vec![Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        )]
+        .into_iter()
+        .collect();
+        let catalog = PredicateCatalog::from_instance(&instance).unwrap();
+        let select = parse_select("SELECT c0 FROM Parent WHERE c1 = 'bob'").unwrap();
+
+        let plan = plan_select(&select, &catalog).unwrap();
+        assert_eq!(plan.output_schema().len(), 1);
+    }
+}

src/relational/mod.rs

@@ -0,0 +1,9 @@
+//! Relational data model scaffolding for future SQL and planner work.
+
+mod row;
+mod schema;
+mod value;
+
+pub use row::{ResultSet, Row};
+pub use schema::{DataType, Field, Schema};
+pub use value::Value;

src/relational/row.rs

@@ -0,0 +1,40 @@
+use super::{Schema, Value};
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Row {
+    values: Vec<Value>,
+}
+
+impl Row {
+    pub fn new(values: Vec<Value>) -> Self {
+        Self { values }
+    }
+
+    pub fn values(&self) -> &[Value] {
+        &self.values
+    }
+
+    pub fn get(&self, index: usize) -> Option<&Value> {
+        self.values.get(index)
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct ResultSet {
+    schema: Schema,
+    rows: Vec<Row>,
+}
+
+impl ResultSet {
+    pub fn new(schema: Schema, rows: Vec<Row>) -> Self {
+        Self { schema, rows }
+    }
+
+    pub fn schema(&self) -> &Schema {
+        &self.schema
+    }
+
+    pub fn rows(&self) -> &[Row] {
+        &self.rows
+    }
+}

src/relational/schema.rs

@@ -0,0 +1,92 @@
+use std::fmt;
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum DataType {
+    Text,
+    Boolean,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Field {
+    name: String,
+    data_type: DataType,
+    nullable: bool,
+}
+
+impl Field {
+    pub fn new(name: impl Into<String>, data_type: DataType, nullable: bool) -> Self {
+        Self {
+            name: name.into(),
+            data_type,
+            nullable,
+        }
+    }
+
+    pub fn name(&self) -> &str {
+        &self.name
+    }
+
+    pub fn data_type(&self) -> &DataType {
+        &self.data_type
+    }
+
+    pub fn nullable(&self) -> bool {
+        self.nullable
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Default)]
+pub struct Schema {
+    fields: Vec<Field>,
+}
+
+impl Schema {
+    pub fn new(fields: Vec<Field>) -> Self {
+        Self { fields }
+    }
+
+    pub fn fields(&self) -> &[Field] {
+        &self.fields
+    }
+
+    pub fn len(&self) -> usize {
+        self.fields.len()
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.fields.is_empty()
+    }
+
+    pub fn index_of(&self, name: &str) -> Option<usize> {
+        self.fields.iter().position(|field| field.name() == name)
+    }
+}
+
+impl fmt::Display for Schema {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let fields = self
+            .fields
+            .iter()
+            .map(|field| field.name().to_string())
+            .collect::<Vec<_>>()
+            .join(", ");
+        write!(f, "[{}]", fields)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn schema_resolves_columns_by_name() {
+        let schema = Schema::new(vec![
+            Field::new("c0", DataType::Text, false),
+            Field::new("c1", DataType::Text, true),
+        ]);
+
+        assert_eq!(schema.index_of("c0"), Some(0));
+        assert_eq!(schema.index_of("c1"), Some(1));
+        assert_eq!(schema.index_of("missing"), None);
+    }
+}

src/relational/value.rs

@@ -0,0 +1,37 @@
+use std::fmt;
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum Value {
+    Text(String),
+    Boolean(bool),
+    Null,
+}
+
+impl Value {
+    pub fn text(value: impl Into<String>) -> Self {
+        Self::Text(value.into())
+    }
+
+    pub fn is_null(&self) -> bool {
+        matches!(self, Self::Null)
+    }
+
+    pub fn sql_eq(&self, other: &Self) -> Option<bool> {
+        match (self, other) {
+            (Self::Null, _) | (_, Self::Null) => None,
+            (Self::Text(left), Self::Text(right)) => Some(left == right),
+            (Self::Boolean(left), Self::Boolean(right)) => Some(left == right),
+            (Self::Text(_), Self::Boolean(_)) | (Self::Boolean(_), Self::Text(_)) => Some(false),
+        }
+    }
+}
+
+impl fmt::Display for Value {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::Text(value) => write!(f, "{}", value),
+            Self::Boolean(value) => write!(f, "{}", value),
+            Self::Null => write!(f, "NULL"),
+        }
+    }
+}

src/sql/ast.rs

@@ -0,0 +1,34 @@
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Select {
+    pub projection: Vec<SelectItem>,
+    pub from: String,
+    pub selection: Option<Expr>,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum SelectItem {
+    Wildcard,
+    Expr { expr: Expr, alias: Option<String> },
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Expr {
+    Identifier(String),
+    Literal(Literal),
+    Binary {
+        left: Box<Expr>,
+        op: BinaryOp,
+        right: Box<Expr>,
+    },
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Literal {
+    String(String),
+    Null,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum BinaryOp {
+    Eq,
+}

src/sql/mod.rs

@@ -0,0 +1,4 @@
+//! Minimal SQL front-end scaffolding.
+
+pub mod ast;
+pub mod parser;

src/sql/parser.rs

@@ -0,0 +1,275 @@
+use std::error::Error;
+use std::fmt;
+
+use super::ast::{BinaryOp, Expr, Literal, Select, SelectItem};
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum ParseError {
+    UnexpectedEnd,
+    ExpectedToken(&'static str),
+    ExpectedIdentifier,
+    UnexpectedToken(String),
+    UnterminatedString,
+}
+
+impl fmt::Display for ParseError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::UnexpectedEnd => write!(f, "unexpected end of input"),
+            Self::ExpectedToken(token) => write!(f, "expected `{}`", token),
+            Self::ExpectedIdentifier => write!(f, "expected identifier"),
+            Self::UnexpectedToken(token) => write!(f, "unexpected token `{}`", token),
+            Self::UnterminatedString => write!(f, "unterminated string literal"),
+        }
+    }
+}
+
+impl Error for ParseError {}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+enum Token {
+    Select,
+    From,
+    Where,
+    Null,
+    Identifier(String),
+    String(String),
+    Star,
+    Comma,
+    Eq,
+}
+
+pub fn parse_select(input: &str) -> Result<Select, ParseError> {
+    let tokens = tokenize(input)?;
+    let mut parser = Parser::new(tokens);
+    parser.parse_select()
+}
+
+struct Parser {
+    tokens: Vec<Token>,
+    index: usize,
+}
+
+impl Parser {
+    fn new(tokens: Vec<Token>) -> Self {
+        Self { tokens, index: 0 }
+    }
+
+    fn parse_select(&mut self) -> Result<Select, ParseError> {
+        self.expect_keyword(Token::Select, "SELECT")?;
+        let projection = self.parse_projection()?;
+        self.expect_keyword(Token::From, "FROM")?;
+        let from = self.expect_identifier()?;
+        let selection = if self.peek() == Some(&Token::Where) {
+            self.index += 1;
+            Some(self.parse_expr()?)
+        } else {
+            None
+        };
+
+        if let Some(token) = self.peek() {
+            return Err(ParseError::UnexpectedToken(render_token(token)));
+        }
+
+        Ok(Select {
+            projection,
+            from,
+            selection,
+        })
+    }
+
+    fn parse_projection(&mut self) -> Result<Vec<SelectItem>, ParseError> {
+        let mut items = Vec::new();
+
+        loop {
+            let item = match self.next().ok_or(ParseError::UnexpectedEnd)? {
+                Token::Star => SelectItem::Wildcard,
+                Token::Identifier(name) => SelectItem::Expr {
+                    expr: Expr::Identifier(name),
+                    alias: None,
+                },
+                other => return Err(ParseError::UnexpectedToken(render_token(&other))),
+            };
+            items.push(item);
+
+            if self.peek() == Some(&Token::Comma) {
+                self.index += 1;
+                continue;
+            }
+            break;
+        }
+
+        Ok(items)
+    }
+
+    fn parse_expr(&mut self) -> Result<Expr, ParseError> {
+        let left = self.parse_operand()?;
+        match self.next().ok_or(ParseError::UnexpectedEnd)? {
+            Token::Eq => {
+                let right = self.parse_operand()?;
+                Ok(Expr::Binary {
+                    left: Box::new(left),
+                    op: BinaryOp::Eq,
+                    right: Box::new(right),
+                })
+            }
+            other => Err(ParseError::UnexpectedToken(render_token(&other))),
+        }
+    }
+
+    fn parse_operand(&mut self) -> Result<Expr, ParseError> {
+        match self.next().ok_or(ParseError::UnexpectedEnd)? {
+            Token::Identifier(name) => Ok(Expr::Identifier(name)),
+            Token::String(value) => Ok(Expr::Literal(Literal::String(value))),
+            Token::Null => Ok(Expr::Literal(Literal::Null)),
+            other => Err(ParseError::UnexpectedToken(render_token(&other))),
+        }
+    }
+
+    fn expect_keyword(&mut self, token: Token, label: &'static str) -> Result<(), ParseError> {
+        let next = self.next().ok_or(ParseError::UnexpectedEnd)?;
+        if next == token {
+            Ok(())
+        } else {
+            Err(ParseError::ExpectedToken(label))
+        }
+    }
+
+    fn expect_identifier(&mut self) -> Result<String, ParseError> {
+        match self.next().ok_or(ParseError::UnexpectedEnd)? {
+            Token::Identifier(name) => Ok(name),
+            _ => Err(ParseError::ExpectedIdentifier),
+        }
+    }
+
+    fn peek(&self) -> Option<&Token> {
+        self.tokens.get(self.index)
+    }
+
+    fn next(&mut self) -> Option<Token> {
+        let token = self.tokens.get(self.index).cloned();
+        if token.is_some() {
+            self.index += 1;
+        }
+        token
+    }
+}
+
+fn tokenize(input: &str) -> Result<Vec<Token>, ParseError> {
+    let mut chars = input.chars().peekable();
+    let mut tokens = Vec::new();
+
+    while let Some(ch) = chars.peek().copied() {
+        if ch.is_whitespace() {
+            chars.next();
+            continue;
+        }
+
+        match ch {
+            '*' => {
+                chars.next();
+                tokens.push(Token::Star);
+            }
+            ',' => {
+                chars.next();
+                tokens.push(Token::Comma);
+            }
+            '=' => {
+                chars.next();
+                tokens.push(Token::Eq);
+            }
+            '\'' => tokens.push(Token::String(parse_string(&mut chars)?)),
+            ch if is_identifier_start(ch) => {
+                let ident = parse_identifier(&mut chars);
+                let token = match ident.to_ascii_uppercase().as_str() {
+                    "SELECT" => Token::Select,
+                    "FROM" => Token::From,
+                    "WHERE" => Token::Where,
+                    "NULL" => Token::Null,
+                    _ => Token::Identifier(ident),
+                };
+                tokens.push(token);
+            }
+            other => return Err(ParseError::UnexpectedToken(other.to_string())),
+        }
+    }
+
+    Ok(tokens)
+}
+
+fn parse_string<I>(chars: &mut std::iter::Peekable<I>) -> Result<String, ParseError>
+where
+    I: Iterator<Item = char>,
+{
+    let mut value = String::new();
+    let quote = chars.next();
+    if quote != Some('\'') {
+        return Err(ParseError::ExpectedToken("'"));
+    }
+
+    while let Some(ch) = chars.next() {
+        if ch == '\'' {
+            if chars.peek() == Some(&'\'') {
+                chars.next();
+                value.push('\'');
+                continue;
+            }
+            return Ok(value);
+        }
+        value.push(ch);
+    }
+
+    Err(ParseError::UnterminatedString)
+}
+
+fn parse_identifier<I>(chars: &mut std::iter::Peekable<I>) -> String
+where
+    I: Iterator<Item = char>,
+{
+    let mut ident = String::new();
+    while let Some(ch) = chars.peek().copied() {
+        if is_identifier_part(ch) {
+            ident.push(ch);
+            chars.next();
+        } else {
+            break;
+        }
+    }
+    ident
+}
+
+fn is_identifier_start(ch: char) -> bool {
+    ch.is_ascii_alphabetic() || ch == '_'
+}
+
+fn is_identifier_part(ch: char) -> bool {
+    ch.is_ascii_alphanumeric() || ch == '_'
+}
+
+fn render_token(token: &Token) -> String {
+    match token {
+        Token::Select => "SELECT".to_string(),
+        Token::From => "FROM".to_string(),
+        Token::Where => "WHERE".to_string(),
+        Token::Null => "NULL".to_string(),
+        Token::Identifier(name) => name.clone(),
+        Token::String(value) => format!("'{}'", value),
+        Token::Star => "*".to_string(),
+        Token::Comma => ",".to_string(),
+        Token::Eq => "=".to_string(),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn parses_select_with_filter() {
+        let select = parse_select("SELECT c0 FROM Parent WHERE c1 = 'bob'").unwrap();
+
+        assert_eq!(select.from, "Parent");
+        assert_eq!(select.projection.len(), 1);
+        assert!(select.selection.is_some());
+    }
+}

tests/sql_pipeline_tests.rs

@@ -0,0 +1,67 @@
+use query_engine::catalog::PredicateCatalog;
+use query_engine::execution::execute;
+use query_engine::planner::sql::plan_select;
+use query_engine::sql::parser::parse_select;
+use query_engine::{Atom, Instance, Term};
+
+fn parent_instance() -> Instance {
+    vec![
+        Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        ),
+        Atom::new(
+            "Parent",
+            vec![Term::constant("bob"), Term::constant("carol")],
+        ),
+    ]
+    .into_iter()
+    .collect()
+}
+
+#[test]
+fn select_star_scans_predicate_as_table() {
+    let instance = parent_instance();
+    let catalog = PredicateCatalog::from_instance(&instance).unwrap();
+    let select = parse_select("SELECT * FROM Parent").unwrap();
+
+    let plan = plan_select(&select, &catalog).unwrap();
+    let result = execute(&plan, &instance).unwrap();
+
+    assert_eq!(result.schema().len(), 2);
+    assert_eq!(result.rows().len(), 2);
+    assert_eq!(result.rows()[0].values().len(), 2);
+}
+
+#[test]
+fn select_projection_keeps_requested_columns() {
+    let instance = parent_instance();
+    let catalog = PredicateCatalog::from_instance(&instance).unwrap();
+    let select = parse_select("SELECT c0 FROM Parent").unwrap();
+
+    let plan = plan_select(&select, &catalog).unwrap();
+    let result = execute(&plan, &instance).unwrap();
+
+    assert_eq!(result.schema().len(), 1);
+    assert_eq!(result.rows().len(), 2);
+    let mut values = result
+        .rows()
+        .iter()
+        .map(|row| format!("{}", row.values()[0]))
+        .collect::<Vec<_>>();
+    values.sort();
+    assert_eq!(values, vec!["alice".to_string(), "bob".to_string()]);
+}
+
+#[test]
+fn select_where_filters_rows() {
+    let instance = parent_instance();
+    let catalog = PredicateCatalog::from_instance(&instance).unwrap();
+    let select = parse_select("SELECT c0 FROM Parent WHERE c1 = 'bob'").unwrap();
+
+    let plan = plan_select(&select, &catalog).unwrap();
+    let result = execute(&plan, &instance).unwrap();
+
+    assert_eq!(result.rows().len(), 1);
+    assert_eq!(format!("{}", result.rows()[0].values()[0]), "alice");
+}