The base commit

.editorconfig

@@ -0,0 +1,22 @@
+root = true
+
+[*]
+charset = utf-8
+end_of_line = lf
+indent_style = space
+indent_size = 4
+insert_final_newline = true
+trim_trailing_whitespace = true
+
+[*.{rs,py}]
+max_line_length = 100
+
+[*.md]
+max_line_length = 150
+trim_trailing_whitespace = false
+
+[*.sh]
+indent_size = 2
+
+[*.{yaml,yml,json}]
+indent_size = 2

.gitattributes

@@ -0,0 +1,38 @@
+* text=auto eol=lf
+
+*.go text
+*.mod text
+*.sum text
+*.md text
+*.rst text
+*.json text
+*.yaml text
+*.yml text
+*.toml text
+*.sh text eol=lf
+*.html text
+*.css text
+*.js text
+*.svg text
+*.xml text
+
+*.png filter=lfs diff=lfs merge=lfs -text
+*.jpg filter=lfs diff=lfs merge=lfs -text
+*.jpeg filter=lfs diff=lfs merge=lfs -text
+*.gif filter=lfs diff=lfs merge=lfs -text
+*.ico filter=lfs diff=lfs merge=lfs -text
+*.mp4 filter=lfs diff=lfs merge=lfs -text
+*.mov filter=lfs diff=lfs merge=lfs -text
+*.zip filter=lfs diff=lfs merge=lfs -text
+*.tar filter=lfs diff=lfs merge=lfs -text
+*.gz filter=lfs diff=lfs merge=lfs -text
+*.tgz filter=lfs diff=lfs merge=lfs -text
+*.ttf filter=lfs diff=lfs merge=lfs -text
+*.woff filter=lfs diff=lfs merge=lfs -text
+*.woff2 filter=lfs diff=lfs merge=lfs -text
+*.exe filter=lfs diff=lfs merge=lfs -text
+*.dll filter=lfs diff=lfs merge=lfs -text
+*.so filter=lfs diff=lfs merge=lfs -text
+*.out filter=lfs diff=lfs merge=lfs -text
+*.a filter=lfs diff=lfs merge=lfs -text
+*.o filter=lfs diff=lfs merge=lfs -text

.gitignore

@@ -0,0 +1,85 @@
+# Python specific
+__pycache__/
+*.py[cod]
+*$py.class
+
+# Virtual environments
+.env/
+env/
+.venv/
+venv/
+
+# Packaging and distribution files
+.Python
+build/
+dist/
+*.egg-info/
+*.egg
+MANIFEST
+
+# Dependency directories
+develop-eggs/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+.installed.cfg
+
+# Test and coverage reports
+htmlcov/
+.tox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+.hypothesis/
+.pytest_cache/
+
+# IDE specific files and directories
+.idea/
+*.iml
+.vscode/
+
+# Jupyter Notebook files
+.ipynb_checkpoints
+
+# Temporary files created by editors and the system and folders to ignore
+*.swp
+*~
+*.bak
+*.tmp
+temp/
+tmp/
+
+# Database files (SQLite, DuckDB, etc.)
+*.duckdb
+*.db
+*.wal
+*.sqlite
+
+# Dependency lock files (uncomment to ignore)
+poetry.lock
+
+# Rust specific
+/target/
+.cargo-ok
+cobertura.xml
+tarpaulin-report.html
+
+# Comment out the next line if you want to checkin your lock file for Cargo
+Cargo.lock
+
+# Misc
+.DS_Store
+.benchmarks
+.env
+.claude/
+*.proptest-regressions
+.codex

.pre-commit-config.yaml

@@ -0,0 +1,43 @@
+default_stages: [ pre-push ]
+fail_fast: false
+exclude: '^(benches/|tests/|examples/|docs/)'
+
+repos:
+  - repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v5.0.0
+    hooks:
+      - id: trailing-whitespace
+        args: [ --markdown-linebreak-ext=md ]
+      - id: end-of-file-fixer
+      - id: mixed-line-ending
+      - id: check-merge-conflict
+      - id: check-added-large-files
+      - id: detect-private-key
+      - id: check-yaml
+      - id: check-toml
+      - id: check-json
+      - id: check-docstring-first
+      - id: pretty-format-json
+        args: [ --autofix, --no-sort-keys ]
+
+  - repo: local
+    hooks:
+      - id: format
+        name: Format Code
+        entry: make format
+        language: system
+        pass_filenames: false
+        stages: [ pre-commit ]
+
+      - id: lint
+        name: Check Code Style
+        entry: make lint
+        language: system
+        pass_filenames: false
+        stages: [ pre-commit ]
+
+      - id: test
+        name: Run Tests
+        entry: make nexttest
+        language: system
+        pass_filenames: false

AGENTS.md

@@ -0,0 +1,206 @@
+# AGENTS.md
+
+This file provides guidance to coding agents collaborating on this repository.
+
+## Mission
+
+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.
+
+Priorities, in order:
+
+1. Correctness of reasoning and query semantics.
+2. Clear architectural boundaries between front-end, planning, and execution layers.
+3. Termination guarantees for chase-based rule evaluation.
+4. Performance and scalability.
+5. Clear, maintainable, idiomatic Rust code.
+
+## Core Rules
+
+- Use English for code, comments, docs, and tests.
+- Keep mutable state inside well-defined structs; avoid global mutable state.
+- Prefer small, focused changes over large refactoring.
+- Add comments only when they clarify non-obvious behavior.
+- Follow Rust idioms: use `Result` for errors, iterators over manual loops, etc.
+- Do not describe unimplemented subsystems as if they already exist.
+
+Quick examples:
+
+- Good: add a planning data type behind a focused module boundary.
+- Good: add a new chase variant by extending the existing strategy/config model.
+- Bad: mix parsing, planning, and execution concerns in one module.
+- Bad: add global configuration that affects unrelated engine components.
+
+
+## Writing Style
+
+- Use Oxford commas in inline lists: "a, b, and c" not "a, b, c".
+- Do not use em dashes. Restructure the sentence, or use a colon or semicolon instead.
+- Avoid colorful adjectives and adverbs. Write "TCP proxy" not "lightweight TCP proxy", "scoring components" not "transparent scoring components".
+- Use noun phrases for checklist items, not imperative verbs. Write "redundant index detection" not "detect redundant indexes".
+- Headings in Markdown files must be in the title case: "Build from Source" not "Build from source". Minor words (a, an, the, and, but, or, for, in,
+  on, at, to, by, of) stay lowercase unless they are the first word.
+
+## Repository Layout
+
+- `src/`: core implementation.
+- `src/chase/`: chase and rule-evaluation modules.
+    - `term.rs`: terms (constants, nulls, variables).
+    - `atom.rs`: atoms (predicate applied to terms).
+    - `instance.rs`: fact storage and validation.
+    - `rule.rs`: TGDs, EGDs, equalities, and builders.
+    - `substitution.rs`: variable bindings and unification.
+    - `engine.rs`: chase execution and configuration.
+    - `union_find.rs`: equality merging support.
+- `src/frontend/`: lightweight interactive surface for scripts, REPL, and local web UI.
+- `tests/`: integration, regression, and property-based tests.
+
+## Architecture Constraints
+
+- Treat the current chase subsystem as one engine component, not the entire long-term architecture.
+- `Instance` holds the fact state as ground atoms.
+- `Rule` and `Egd` represent declarative constraints used by the chase subsystem.
+- 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`).
+- 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.
+
+## Rust Conventions
+
+- Target stable Rust (edition 2024, rust-version 1.92).
+- Use `#[derive(...)]` for common traits where appropriate.
+- Prefer `&str` over `String` in function parameters when ownership is not needed.
+- Use `impl Trait` for return types when the concrete type is an implementation detail.
+- Run `cargo clippy` and address warnings before committing.
+
+## Required Validation
+
+Run these checks for any non-trivial change:
+
+1. `cargo test`
+2. `cargo clippy --all-targets --all-features -- -D warnings`
+3. `cargo fmt --check`
+
+For performance-sensitive changes:
+
+1. Add benchmarks if they do not exist.
+2. Compare before/after performance.
+
+## First Contribution Flow
+
+Use this sequence for your first change:
+
+1. Read `src/lib.rs` plus the relevant module files.
+2. Implement the smallest possible code change.
+3. Add or update tests that fail before and pass after.
+4. Run `cargo test`.
+5. Run `cargo clippy --all-targets --all-features -- -D warnings`.
+6. Update docs if public API behavior changed.
+
+Example scopes that are good first tasks:
+
+- Add tests for an edge case in unification.
+- 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.
+
+## Testing Expectations
+
+- No semantics-changing logic update is complete without tests.
+- Unit tests go in `#[cfg(test)] mod tests` within each module.
+- 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`.
+- Do not merge code that breaks existing tests.
+
+Minimal unit-test checklist for chase-related behavior:
+
+1. Create an `Instance` with relevant facts.
+2. Define rules using `RuleBuilder`.
+3. Run `chase(instance, &rules)`.
+4. Assert on `result.terminated`, `result.instance`, and derived facts.
+
+Example test skeleton:
+
+```rust
+#[test]
+fn test_example() {
+    let instance: Instance = vec![
+        Atom::new("Pred", vec![Term::constant("a")]),
+    ].into_iter().collect();
+
+    let rule = RuleBuilder::new()
+        .when("Pred", vec![Term::var("X")])
+        .then("Derived", vec![Term::var("X")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+    assert_eq!(result.instance.facts_for_predicate("Derived").len(), 1);
+}
+```
+
+## Change Design Checklist
+
+Before coding:
+
+1. Confirm whether the change affects reasoning semantics, planning boundaries, or termination.
+2. Identify affected tests.
+3. Consider impact on API stability.
+4. Avoid overstating roadmap progress in code comments or docs.
+
+Before submitting:
+
+1. Verify `cargo test` passes.
+2. Verify `cargo clippy --all-targets --all-features -- -D warnings` passes.
+3. Ensure tests were added or updated where relevant.
+4. Verify docs still match the implemented feature set.
+
+## Review Guidelines (P0/P1 Focus)
+
+Review output should be concise and only include critical issues.
+
+- `P0`: must-fix defects (incorrect reasoning, non-termination, unsound semantics).
+- `P1`: high-priority defects (likely functional bug, performance regression, API breakage, misleading public behavior/docs).
+
+Do not include:
+
+- style-only nitpicks,
+- praise/summary of what is already good,
+- exhaustive restatement of the patch.
+
+Use this review format:
+
+1. `Severity` (`P0`/`P1`)
+2. `File:line`
+3. `Issue`
+4. `Why it matters`
+5. `Minimal fix direction`
+
+## Practical Notes for Agents
+
+- Prefer targeted edits over broad mechanical rewrites.
+- 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 user-facing naming consistent with the repository name: `query-engine` / `query_engine`.
+
+## Commit and PR Hygiene
+
+- Keep commits scoped to one logical change.
+- PR descriptions should include:
+    1. behavioral change summary,
+    2. tests added/updated,
+    3. performance impact (if applicable),
+    4. API changes (if any),
+    5. roadmap or architecture impact (if applicable).
+
+Suggested PR checklist:
+
+- [ ] Tests added/updated for behavior changes
+- [ ] `cargo test` passes
+- [ ] `cargo clippy --all-targets --all-features -- -D warnings` passes
+- [ ] `cargo fmt --check` passes

Cargo.toml

@@ -0,0 +1,56 @@
+[package]
+name = "query-engine"
+version = "0.1.0-alpha.1"
+description = "A playground for experimenting with query engine components in Rust"
+repository = "https://code.obsidian.systems/habedi-work/query-engine"
+license = "BSD-3"
+readme = "README.md"
+edition = "2024"
+rust-version = "1.92"
+publish = false
+
+resolver = "2"
+
+include = [
+    "src/**/*",
+    "Cargo.toml",
+    "README.md",
+    "LICENSE",
+]
+
+[lib]
+name = "query_engine"
+path = "src/lib.rs"
+
+[[bin]]
+name = "query-engine"
+path = "src/main.rs"
+
+[features]
+default = []  # No features enabled by default
+binaries = []
+
+[dependencies]
+
+[dev-dependencies]
+proptest = "1.6"
+
+[profile.release]
+strip = "debuginfo"
+panic = "unwind"
+codegen-units = 1
+lto = true
+
+[profile.test]
+debug = true
+
+[profile.example]
+inherits = "release"
+
+[package.metadata.rustfmt]
+max_width = 100
+hard_tabs = false
+tab_spaces = 4
+
+[workspace]
+members = []

LICENSE

@@ -0,0 +1,11 @@
+Copyright (c) 2026 Obsidian Systems LLC
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Makefile

@@ -0,0 +1,120 @@
+# Variables
+BINARY_NAME := chase-rs
+BINARY := target/release/$(BINARY_NAME)
+DEBUG_PROJ := 0
+RUST_BACKTRACE := 1
+
+# Default target
+.DEFAULT_GOAL := help
+
+.PHONY: help
+help: ## Show help messages for all available targets
+	@grep -E '^[a-zA-Z_-]+:.*## .*$$' Makefile | \
+	awk 'BEGIN {FS = ":.*## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'
+
+.PHONY: format
+format: ## Format Rust files
+	@echo "Formatting Rust files..."
+	@cargo fmt
+
+.PHONY: test
+test: format ## Run the tests
+	@echo "Running tests..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) RUST_BACKTRACE=$(RUST_BACKTRACE) cargo test --all-targets --workspace -- --nocapture
+
+.PHONY: coverage
+coverage: format ## Generate test coverage report
+	@echo "Generating test coverage report..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo tarpaulin --out Xml --out Html
+
+.PHONY: build
+build: format ## Build the binary for the current platform
+	@echo "Building the project..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo build --release
+
+.PHONY: run
+run: build ## Build and run the binary
+	@echo "Running the $(BINARY) binary..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) ./$(BINARY)
+
+.PHONY: repl
+repl: format ## Start the interactive REPL
+	@echo "Starting chase-rs REPL..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- repl
+
+.PHONY: gui
+gui: format ## Start the local GUI at 127.0.0.1:7878
+	@echo "Starting chase-rs GUI on http://127.0.0.1:7878..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- gui
+
+.PHONY: gui-addr
+gui-addr: format ## Start the local GUI at GUI_ADDR=<host:port>
+	@echo "Starting chase-rs GUI on http://$(or $(GUI_ADDR),127.0.0.1:7878)..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- gui $(or $(GUI_ADDR),127.0.0.1:7878)
+
+.PHONY: script
+script: format ## Run a frontend script with SCRIPT=<path>
+	@if [ -z "$(SCRIPT)" ]; then \
+	   echo "Usage: make script SCRIPT=<path>"; \
+	   exit 1; \
+	fi
+	@echo "Running script $(SCRIPT)..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- script $(SCRIPT)
+
+.PHONY: clean
+clean: ## Remove generated and temporary files
+	@echo "Cleaning up..."
+	@cargo clean
+
+.PHONY: install-deps
+install-deps: ## Install development dependencies
+	@echo "Installing dependencies..."
+	@rustup component add rustfmt clippy
+	@cargo install cargo-tarpaulin
+	@cargo install cargo-audit
+	@cargo install cargo-nextest
+
+.PHONY: lint
+lint: format ## Run the linters
+	@echo "Linting Rust files..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) cargo clippy -- -D warnings -D clippy::unwrap_used -D clippy::expect_used
+
+.PHONY: audit
+audit: ## Run security audit on Rust dependencies
+	@echo "Running security audit..."
+	@cargo audit
+
+.PHONY: docs
+docs: format ## Generate the documentation
+	@echo "Generating documentation..."
+	@cargo doc --no-deps --document-private-items
+
+.PHONY: fix-lint
+fix-lint: ## Fix the linter warnings
+	@echo "Fixing linter warnings..."
+	@cargo clippy --fix --allow-dirty --allow-staged --all-targets --workspace
+
+.PHONY: nextest
+nextest: ## Run tests using nextest
+	@echo "Running tests using nextest..."
+	@DEBUG_PROJ=$(DEBUG_PROJ) RUST_BACKTRACE=$(RUST_BACKTRACE) cargo nextest run
+
+.PHONY: setup-hooks
+setup-hooks: ## Install Git hooks (pre-commit)
+	@echo "Setting up Git hooks..."
+	@if ! command -v pre-commit &> /dev/null; then \
+	   echo "pre-commit not found. Please install it using 'pip install pre-commit'"; \
+	   exit 1; \
+	fi
+	@pre-commit install --hook-type pre-commit
+	@pre-commit install --hook-type pre-push
+	@pre-commit install-hooks
+
+.PHONY: test-hooks
+test-hooks: ## Test Git hooks on all files
+	@echo "Testing Git hooks..."
+	@pre-commit run --all-files --show-diff-on-failure
+
+.PHONY: check
+check: format lint test ## Run format, lint, and test
+	@echo "All checks passed."

README.md

@@ -0,0 +1,102 @@
+## Query Engine
+
+An experimental Rust project for building query-engine components.
+
+Right now the repository is centered on a chase-based reasoning core plus a
+small interactive frontend. The broader target shape is a query engine with
+clearer front-end, planning, optimization, and execution boundaries.
+
+### Current scope
+
+- Chase-based rule evaluation over facts, rules, and substitutions
+- Restricted-chase style materialization with active-trigger checks
+- Provenance-oriented explanations for derived answers
+- Script, REPL, and local web UI for experimentation
+
+### Intended direction
+
+The medium-term direction is to evolve this project from a copied
+`chase-rs` codebase into a more general query-engine playground with:
+
+- explicit front-end and parsing layers
+- internal planning representations
+- clearer separation between logical meaning and execution strategy
+- support for multiple query-engine experiments instead of only chase logic
+
+The current code does not yet implement a SQL front end, logical plan, or
+physical plan. The repository naming, docs, and user-facing surfaces now
+reflect that more honestly.
+
+### Quickstart
+
+#### Rust API
+
+```rust
+use query_engine::{Atom, Instance, Term, chase};
+use query_engine::chase::rule::RuleBuilder;
+
+let 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();
+
+let rule1 = RuleBuilder::new()
+    .when("Parent", vec![Term::var("X"), Term::var("Y")])
+    .then("Ancestor", vec![Term::var("X"), Term::var("Y")])
+    .build();
+
+let rule2 = RuleBuilder::new()
+    .when("Ancestor", vec![Term::var("X"), Term::var("Y")])
+    .when("Parent", vec![Term::var("Y"), Term::var("Z")])
+    .then("Ancestor", vec![Term::var("X"), Term::var("Z")])
+    .build();
+
+let result = chase(instance, &[rule1, rule2]);
+
+assert!(result.terminated);
+assert_eq!(result.instance.facts_for_predicate("Ancestor").len(), 3);
+```
+
+#### CLI
+
+```bash
+cargo run -- repl
+cargo run -- gui
+cargo run -- script examples/scripts/ancestor.chase
+```
+
+#### REPL language
+
+```text
+fact Parent(alice, bob).
+rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
+run.
+query Ancestor(?X, ?Y)?
+explain Ancestor(alice, carol)?
+show facts
+show rules
+reset
+help
+```
+
+### Development
+
+For non-trivial changes, run:
+
+```bash
+cargo test
+cargo clippy --all-targets --all-features -- -D warnings
+cargo fmt --check
+```
+
+### Notes
+
+This repository is still centered on a rule-engine core. The longer-term goal
+is to grow it into a broader query-engine project without claiming SQL,
+logical-planning, or physical-planning support before those layers exist.
+
+### License
+
+This project is licensed under [BSD-3](LICENSE).

ROADMAP.md

@@ -0,0 +1,96 @@
+## Project Roadmap
+
+This document tracks the current state and next steps for the repository.
+
+> [!IMPORTANT]
+> The project is still early-stage. Treat this roadmap as directional rather
+> than fixed, and do not read unchecked items as implied existing behavior.
+
+### Current Foundation
+
+- [x] Rust crate and binary named `query_engine` / `query-engine`
+- [x] Core term representation (`Constant`, `Null`, `Variable`)
+- [x] Atom structure (predicate with terms)
+- [x] Fact storage via `Instance`
+- [x] Tuple-generating dependencies (TGDs)
+- [x] Equality-generating dependencies (EGDs)
+- [x] Rule and EGD builders
+- [x] Variable substitutions and atom unification
+- [x] Restricted chase implementation
+- [x] Standard chase implementation
+- [x] Existential variable support (labeled null generation)
+- [x] Multi-atom rule bodies and heads
+- [x] Equality merging with union-find support
+- [x] REPL, script runner, and local web UI
+- [x] Provenance-oriented explanation support
+
+### Near-Term Cleanup
+
+- [ ] Keep all public docs aligned with actual implemented behavior
+- [ ] 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
+
+### Query-Engine Structure
+
+- [ ] Introduce a dedicated logical representation module
+- [ ] Define clear front-end, planning, and execution boundaries
+- [ ] Add engine-level abstractions that are not chase-specific
+- [ ] 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
+- [ ] Add AST types for a structured query front end
+- [ ] Add logical plan node types
+- [ ] Add name resolution and schema validation hooks
+- [ ] Add expression typing and nullability tracking
+
+### Execution and Optimization
+
+- [ ] Introduce physical operator abstractions
+- [ ] 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
+
+### Rule-Engine Evolution
+
+- [x] Restricted chase
+- [x] Standard chase
+- [ ] Oblivious chase
+- [ ] Skolem chase
+- [ ] Core chase
+- [ ] Negative constraints
+- [ ] Stratified negation in rule bodies
+- [ ] Disjunctive heads
+- [ ] Aggregation support in rule evaluation
+- [ ] Semi-naive evaluation
+- [ ] Termination analysis helpers
+
+### Data and Interoperability
+
+- [ ] Fact import/export
+- [ ] File-backed data source experiments
+- [ ] Table-like row or batch abstractions
+- [ ] Stable script/query file format
+- [ ] Integration with external storage or file formats
+
+### Performance and Reliability
+
+- [ ] Predicate indexing for fact lookup
+- [ ] Incremental evaluation
+- [ ] Benchmarks
+- [ ] Fuzzing
+- [ ] Profiling-guided optimization passes
+
+### Testing and Tooling
+
+- [x] Unit tests
+- [x] Integration tests
+- [x] Property-based tests
+- [x] Regression tests
+- [ ] Benchmark coverage
+- [ ] Snapshot-style frontend tests
+- [ ] More planner/executor tests as those layers are added

flake.nix

@@ -0,0 +1,45 @@
+{
+  description = "A playground for experimenting with query engine stuff";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+    rust-overlay = {
+      url = "github:oxalica/rust-overlay";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+  };
+
+  outputs = { self, nixpkgs, flake-utils, rust-overlay }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        overlays = [ (import rust-overlay) ];
+        pkgs = import nixpkgs {
+          inherit system overlays;
+        };
+
+        rustToolchain = pkgs.rust-bin.stable.latest.default.override {
+          extensions = [ "rust-src" "rust-analyzer" "clippy" "rustfmt" ];
+        };
+      in
+      {
+        devShells.default = pkgs.mkShell {
+          buildInputs = [
+            rustToolchain
+            pkgs.pkg-config
+            pkgs.openssl
+          ];
+
+          shellHook = ''
+            echo "chase-rs development shell"
+            echo "Rust: $(rustc --version)"
+          '';
+
+          OPENSSL_DIR = "${pkgs.openssl.dev}";
+          OPENSSL_LIB_DIR = "${pkgs.openssl.out}/lib";
+          OPENSSL_INCLUDE_DIR = "${pkgs.openssl.dev}/include";
+          PKG_CONFIG_PATH = "${pkgs.openssl.dev}/lib/pkgconfig";
+        };
+      }
+    );
+}

pyproject.toml

@@ -0,0 +1,11 @@
+[project]
+name = "query-engine"
+version = "0.1.0"
+description = "The Python environment for the `query-engine` project"
+
+requires-python = ">=3.10,<4.0"
+
+dependencies = [
+    "pre-commit (>=4.2.0,<5.0.0)",
+    "icecream (>=2.1.4,<3.0.0)",
+]

rust-toolchain.toml

@@ -0,0 +1,3 @@
+[toolchain]
+channel = "1.92.0"
+components = ["rustfmt", "clippy", "rust-analyzer"]

src/chase/atom.rs

@@ -0,0 +1,91 @@
+//! Atoms represent predicates applied to terms.
+
+use std::fmt;
+
+use super::term::Term;
+
+/// An atom is a predicate symbol applied to a tuple of terms.
+/// Example: Parent(alice, bob) or Ancestor(?X, ?Y)
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct Atom {
+    /// The predicate name.
+    pub predicate: String,
+    /// The arguments to the predicate.
+    pub terms: Vec<Term>,
+}
+
+impl Atom {
+    /// Create a new atom with the given predicate and terms.
+    pub fn new(predicate: impl Into<String>, terms: Vec<Term>) -> Self {
+        Atom {
+            predicate: predicate.into(),
+            terms,
+        }
+    }
+
+    /// Returns the arity (number of arguments) of this atom.
+    pub fn arity(&self) -> usize {
+        self.terms.len()
+    }
+
+    /// Returns true if this atom is ground (contains no variables).
+    pub fn is_ground(&self) -> bool {
+        self.terms.iter().all(|t| t.is_ground())
+    }
+
+    /// Get all variables in this atom.
+    pub fn variables(&self) -> Vec<&String> {
+        self.terms
+            .iter()
+            .filter_map(|t| match t {
+                Term::Variable(v) => Some(v),
+                _ => None,
+            })
+            .collect()
+    }
+}
+
+impl fmt::Display for Atom {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}(", self.predicate)?;
+        for (i, term) in self.terms.iter().enumerate() {
+            if i > 0 {
+                write!(f, ", ")?;
+            }
+            write!(f, "{}", term)?;
+        }
+        write!(f, ")")
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_atom_creation() {
+        let atom = Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        );
+        assert_eq!(atom.predicate, "Parent");
+        assert_eq!(atom.arity(), 2);
+        assert!(atom.is_ground());
+    }
+
+    #[test]
+    fn test_atom_with_variables() {
+        let atom = Atom::new("Ancestor", vec![Term::var("X"), Term::var("Y")]);
+        assert!(!atom.is_ground());
+        assert_eq!(atom.variables().len(), 2);
+    }
+
+    #[test]
+    fn test_atom_display() {
+        let atom = Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        );
+        assert_eq!(format!("{}", atom), "Parent(alice, bob)");
+    }
+}

src/chase/engine.rs

@@ -0,0 +1,799 @@
+//! Core chase algorithm implementation.
+
+use std::collections::HashSet;
+use std::error::Error;
+use std::fmt;
+
+use super::atom::Atom;
+use super::inference::{NullGenerator, Trigger, apply_rule_head, find_matches, head_is_satisfied};
+use super::instance::Instance;
+use super::rule::{Egd, Rule};
+use super::substitution::Substitution;
+use super::term::Term;
+use super::union_find::{MergeError, UnionFind};
+
+/// Error that can occur during chase with EGDs.
+#[derive(Debug, Clone)]
+pub enum ChaseError {
+    /// EGD tried to equate two different constants.
+    EgdConflict(MergeError),
+}
+
+impl fmt::Display for ChaseError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            ChaseError::EgdConflict(e) => write!(f, "EGD conflict: {}", e),
+        }
+    }
+}
+
+impl Error for ChaseError {
+    fn source(&self) -> Option<&(dyn Error + 'static)> {
+        match self {
+            ChaseError::EgdConflict(e) => Some(e),
+        }
+    }
+}
+
+impl From<MergeError> for ChaseError {
+    fn from(e: MergeError) -> Self {
+        ChaseError::EgdConflict(e)
+    }
+}
+
+/// Result of running the chase algorithm.
+#[derive(Debug)]
+pub struct ChaseResult {
+    /// The final instance after the chase terminates.
+    pub instance: Instance,
+    /// Number of chase steps performed.
+    pub steps: usize,
+    /// Whether the chase terminated (vs hitting a limit).
+    pub terminated: bool,
+    /// Error that occurred during chase (e.g., EGD conflict).
+    pub error: Option<ChaseError>,
+}
+
+/// The variant of chase algorithm to use.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
+pub enum ChaseVariant {
+    /// Standard chase: no trigger tracking, terminates only when no new facts.
+    /// May re-apply rules with the same bindings if heads are satisfied.
+    Standard,
+    /// Restricted chase: uses trigger tracking to avoid re-applying the same
+    /// rule with the same frontier variable bindings. This is the default.
+    #[default]
+    Restricted,
+}
+
+/// Configuration for the chase algorithm.
+#[derive(Debug, Clone)]
+pub struct ChaseConfig {
+    /// Maximum number of chase steps before giving up.
+    pub max_steps: usize,
+    /// The chase variant to use.
+    pub variant: ChaseVariant,
+}
+
+impl Default for ChaseConfig {
+    fn default() -> Self {
+        ChaseConfig {
+            max_steps: 10_000,
+            variant: ChaseVariant::default(),
+        }
+    }
+}
+
+/// Run the restricted chase algorithm (default).
+///
+/// The chase repeatedly applies rules to derive new facts until no more
+/// facts can be derived (fixpoint) or a limit is reached.
+///
+/// This implementation uses a restricted chase style active-trigger check:
+/// a rule fires only when its head is not already satisfied for the current
+/// frontier-variable bindings.
+pub fn chase(instance: Instance, rules: &[Rule]) -> ChaseResult {
+    chase_with_config(instance, rules, ChaseConfig::default())
+}
+
+/// Run the standard chase algorithm (no trigger tracking).
+///
+/// The standard chase applies rules whenever the body matches, without
+/// tracking which rule applications have been performed. It terminates
+/// only when no new facts are derived.
+///
+/// This is simpler but may be less efficient for rules with existentials,
+/// as it doesn't prevent re-checking already-satisfied rule applications.
+pub fn standard_chase(instance: Instance, rules: &[Rule]) -> ChaseResult {
+    let config = ChaseConfig {
+        variant: ChaseVariant::Standard,
+        ..Default::default()
+    };
+    chase_with_config(instance, rules, config)
+}
+
+/// Run the chase with custom configuration.
+pub fn chase_with_config(
+    mut instance: Instance,
+    rules: &[Rule],
+    config: ChaseConfig,
+) -> ChaseResult {
+    let mut null_gen = NullGenerator::seeded_from(&instance, rules);
+    let mut applied_triggers: HashSet<Trigger> = HashSet::new();
+    let mut steps = 0;
+
+    loop {
+        if steps >= config.max_steps {
+            return ChaseResult {
+                instance,
+                steps,
+                terminated: false,
+                error: None,
+            };
+        }
+
+        let new_facts = match config.variant {
+            ChaseVariant::Standard => standard_chase_step(&instance, rules, &mut null_gen),
+            ChaseVariant::Restricted => {
+                restricted_chase_step(&instance, rules, &mut null_gen, &mut applied_triggers)
+            }
+        };
+
+        if new_facts.is_empty() {
+            // Fixpoint reached
+            return ChaseResult {
+                instance,
+                steps,
+                terminated: true,
+                error: None,
+            };
+        }
+
+        for fact in new_facts {
+            instance.add(fact);
+        }
+        steps += 1;
+    }
+}
+
+/// Perform a single standard chase step: apply rules without trigger tracking.
+fn standard_chase_step(
+    instance: &Instance,
+    rules: &[Rule],
+    null_gen: &mut NullGenerator,
+) -> Vec<Atom> {
+    let mut new_facts = Vec::new();
+
+    for rule in rules {
+        // Find all ways to match the rule body against the instance
+        let matches = find_matches(instance, &rule.body);
+
+        for subst in matches {
+            // In standard chase, we only check if head is satisfied
+            if head_is_satisfied(instance, rule, &subst) {
+                continue;
+            }
+
+            // Generate head atoms with this substitution
+            let derived = apply_rule_head(rule, &subst, null_gen);
+
+            for fact in derived {
+                if !instance.contains(&fact) {
+                    new_facts.push(fact);
+                }
+            }
+        }
+    }
+
+    new_facts
+}
+
+/// Perform a single restricted chase step: use trigger tracking to avoid redundant applications.
+fn restricted_chase_step(
+    instance: &Instance,
+    rules: &[Rule],
+    null_gen: &mut NullGenerator,
+    applied_triggers: &mut HashSet<Trigger>,
+) -> Vec<Atom> {
+    let mut new_facts = Vec::new();
+
+    for (rule_idx, rule) in rules.iter().enumerate() {
+        // Find all ways to match the rule body against the instance
+        let matches = find_matches(instance, &rule.body);
+
+        for subst in matches {
+            // Create a trigger to check if we've already applied this
+            let trigger = Trigger::new(rule_idx, rule, &subst);
+
+            // Skip if already applied in this materialization
+            if applied_triggers.contains(&trigger) {
+                continue;
+            }
+
+            if head_is_satisfied(instance, rule, &subst) {
+                continue;
+            }
+
+            // Mark this trigger as applied
+            applied_triggers.insert(trigger);
+
+            // Generate head atoms with this substitution
+            let derived = apply_rule_head(rule, &subst, null_gen);
+
+            for fact in derived {
+                if !instance.contains(&fact) {
+                    new_facts.push(fact);
+                }
+            }
+        }
+    }
+
+    new_facts
+}
+
+/// A trigger for EGD applications, tracking which EGD was applied with which body bindings.
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+struct EgdTrigger {
+    egd_index: usize,
+    /// All body variable bindings for the EGD.
+    body_bindings: Vec<(String, Term)>,
+}
+
+impl EgdTrigger {
+    fn new(egd_index: usize, egd: &Egd, subst: &Substitution) -> Self {
+        let body_vars = egd.body_variables();
+        let mut bindings: Vec<_> = body_vars
+            .into_iter()
+            .filter_map(|v| subst.get(&v).map(|t| (v, t.clone())))
+            .collect();
+        bindings.sort_by(|a, b| a.0.cmp(&b.0));
+
+        EgdTrigger {
+            egd_index,
+            body_bindings: bindings,
+        }
+    }
+}
+
+/// Apply EGDs to the instance, returning any merge error that occurs.
+fn apply_egds(
+    instance: &Instance,
+    egds: &[Egd],
+    uf: &mut UnionFind,
+    applied_egd_triggers: &mut HashSet<EgdTrigger>,
+) -> Result<bool, MergeError> {
+    let mut made_changes = false;
+
+    for (egd_idx, egd) in egds.iter().enumerate() {
+        let matches = find_matches(instance, &egd.body);
+
+        for subst in matches {
+            let trigger = EgdTrigger::new(egd_idx, egd, &subst);
+
+            if applied_egd_triggers.contains(&trigger) {
+                continue;
+            }
+            applied_egd_triggers.insert(trigger);
+
+            // Get the terms that should be equal
+            let left = subst.apply_term(&egd.equality.left);
+            let right = subst.apply_term(&egd.equality.right);
+
+            // Merge them in the union-find
+            uf.merge(&left, &right)?;
+            made_changes = true;
+        }
+    }
+
+    Ok(made_changes)
+}
+
+/// Run chase with both TGDs and EGDs.
+///
+/// The chase alternates between:
+/// 1. Applying TGDs to derive new facts
+/// 2. Applying EGDs to enforce equalities
+/// 3. Canonicalizing the instance to reflect merged nulls
+///
+/// Terminates when fixpoint is reached or an error occurs (EGD conflict).
+pub fn chase_with_egds(instance: Instance, tgds: &[Rule], egds: &[Egd]) -> ChaseResult {
+    chase_full(instance, tgds, egds, ChaseConfig::default())
+}
+
+/// Run the full chase with TGDs, EGDs, and custom configuration.
+pub fn chase_full(
+    mut instance: Instance,
+    tgds: &[Rule],
+    egds: &[Egd],
+    config: ChaseConfig,
+) -> ChaseResult {
+    let mut null_gen = NullGenerator::seeded_from(&instance, tgds);
+    let mut applied_triggers: HashSet<Trigger> = HashSet::new();
+    let mut applied_egd_triggers: HashSet<EgdTrigger> = HashSet::new();
+    let mut uf = UnionFind::new();
+    let mut steps = 0;
+
+    loop {
+        if steps >= config.max_steps {
+            return ChaseResult {
+                instance,
+                steps,
+                terminated: false,
+                error: None,
+            };
+        }
+
+        // Apply TGDs
+        let new_facts = match config.variant {
+            ChaseVariant::Standard => standard_chase_step(&instance, tgds, &mut null_gen),
+            ChaseVariant::Restricted => {
+                restricted_chase_step(&instance, tgds, &mut null_gen, &mut applied_triggers)
+            }
+        };
+
+        let tgd_changes = !new_facts.is_empty();
+        for fact in new_facts {
+            instance.add(fact);
+        }
+
+        // Apply EGDs
+        let egd_result = apply_egds(&instance, egds, &mut uf, &mut applied_egd_triggers);
+
+        match egd_result {
+            Err(e) => {
+                return ChaseResult {
+                    instance,
+                    steps,
+                    terminated: false,
+                    error: Some(ChaseError::EgdConflict(e)),
+                };
+            }
+            Ok(egd_changes) => {
+                // Canonicalize instance if EGDs made changes
+                if egd_changes {
+                    instance = instance.canonicalize(&mut uf);
+                }
+
+                // Check for fixpoint
+                if !tgd_changes && !egd_changes {
+                    return ChaseResult {
+                        instance,
+                        steps,
+                        terminated: true,
+                        error: None,
+                    };
+                }
+            }
+        }
+
+        steps += 1;
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::chase::rule::RuleBuilder;
+
+    #[test]
+    fn test_simple_chase() {
+        // Initial facts
+        let 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();
+
+        // Rule: Parent(X, Y) -> Ancestor(X, Y)
+        let rule1 = RuleBuilder::new()
+            .when("Parent", vec![Term::var("X"), Term::var("Y")])
+            .then("Ancestor", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        // Rule: Ancestor(X, Y), Parent(Y, Z) -> Ancestor(X, Z)
+        let rule2 = RuleBuilder::new()
+            .when("Ancestor", vec![Term::var("X"), Term::var("Y")])
+            .when("Parent", vec![Term::var("Y"), Term::var("Z")])
+            .then("Ancestor", vec![Term::var("X"), Term::var("Z")])
+            .build();
+
+        let result = chase(instance, &[rule1, rule2]);
+
+        assert!(result.terminated);
+
+        // Check derived facts
+        let ancestors = result.instance.facts_for_predicate("Ancestor");
+        assert_eq!(ancestors.len(), 3); // alice->bob, bob->carol, alice->carol
+    }
+
+    #[test]
+    fn test_chase_with_existentials() {
+        // Initial facts
+        let instance: Instance = vec![Atom::new("Person", vec![Term::constant("alice")])]
+            .into_iter()
+            .collect();
+
+        // Rule: Person(X) -> HasSSN(X, Y) where Y is existential
+        let rule = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("HasSSN", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        assert!(result.terminated);
+
+        let has_ssn = result.instance.facts_for_predicate("HasSSN");
+        assert_eq!(has_ssn.len(), 1);
+
+        // Check that a null was generated
+        let fact = has_ssn[0];
+        assert!(matches!(fact.terms[1], Term::Null(_)));
+    }
+
+    #[test]
+    fn test_chase_multiple_existentials() {
+        // Test that each person gets their own SSN
+        let instance: Instance = vec![
+            Atom::new("Person", vec![Term::constant("alice")]),
+            Atom::new("Person", vec![Term::constant("bob")]),
+        ]
+        .into_iter()
+        .collect();
+
+        let rule = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("HasSSN", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        assert!(result.terminated);
+
+        let has_ssn = result.instance.facts_for_predicate("HasSSN");
+        assert_eq!(has_ssn.len(), 2);
+
+        // Verify different nulls were generated
+        let nulls: Vec<_> = has_ssn.iter().map(|f| &f.terms[1]).collect();
+        assert_ne!(nulls[0], nulls[1]);
+    }
+
+    #[test]
+    fn test_empty_chase() {
+        let instance = Instance::new();
+        let result = chase(instance, &[]);
+
+        assert!(result.terminated);
+        assert_eq!(result.steps, 0);
+    }
+
+    #[test]
+    fn test_chase_fixpoint() {
+        // With no applicable rules, chase should terminate immediately
+        let instance: Instance = vec![Atom::new("Fact", vec![Term::constant("a")])]
+            .into_iter()
+            .collect();
+
+        let rule = RuleBuilder::new()
+            .when("Other", vec![Term::var("X")])
+            .then("Derived", vec![Term::var("X")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        assert!(result.terminated);
+        assert_eq!(result.instance.len(), 1);
+    }
+
+    #[test]
+    fn test_chase_no_duplicate_applications() {
+        // Ensure the same rule isn't applied twice for the same body match
+        let instance: Instance = vec![Atom::new("A", vec![Term::constant("x")])]
+            .into_iter()
+            .collect();
+
+        // A(X) -> B(X, Y) - should only fire once per X value
+        let rule = RuleBuilder::new()
+            .when("A", vec![Term::var("X")])
+            .then("B", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let result = chase(instance, &[rule]);
+
+        assert!(result.terminated);
+        assert_eq!(result.instance.facts_for_predicate("B").len(), 1);
+    }
+
+    #[test]
+    fn test_standard_chase_basic() {
+        // Test standard chase with datalog rules
+        let 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();
+
+        let rule1 = RuleBuilder::new()
+            .when("Parent", vec![Term::var("X"), Term::var("Y")])
+            .then("Ancestor", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let rule2 = RuleBuilder::new()
+            .when("Ancestor", vec![Term::var("X"), Term::var("Y")])
+            .when("Parent", vec![Term::var("Y"), Term::var("Z")])
+            .then("Ancestor", vec![Term::var("X"), Term::var("Z")])
+            .build();
+
+        let result = standard_chase(instance, &[rule1, rule2]);
+
+        assert!(result.terminated);
+        let ancestors = result.instance.facts_for_predicate("Ancestor");
+        assert_eq!(ancestors.len(), 3);
+    }
+
+    #[test]
+    fn test_standard_and_restricted_reach_same_fixpoint() {
+        // For datalog rules (no existentials), both should reach the same result
+        let instance: Instance = vec![
+            Atom::new("Edge", vec![Term::constant("a"), Term::constant("b")]),
+            Atom::new("Edge", vec![Term::constant("b"), Term::constant("c")]),
+            Atom::new("Edge", vec![Term::constant("c"), Term::constant("d")]),
+        ]
+        .into_iter()
+        .collect();
+
+        let rule1 = RuleBuilder::new()
+            .when("Edge", vec![Term::var("X"), Term::var("Y")])
+            .then("Path", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let rule2 = RuleBuilder::new()
+            .when("Path", vec![Term::var("X"), Term::var("Y")])
+            .when("Edge", vec![Term::var("Y"), Term::var("Z")])
+            .then("Path", vec![Term::var("X"), Term::var("Z")])
+            .build();
+
+        let rules = vec![rule1, rule2];
+
+        let standard_result = standard_chase(instance.clone(), &rules);
+        let restricted_result = chase(instance, &rules);
+
+        assert!(standard_result.terminated);
+        assert!(restricted_result.terminated);
+
+        // Both should derive the same paths
+        let standard_paths = standard_result.instance.facts_for_predicate("Path");
+        let restricted_paths = restricted_result.instance.facts_for_predicate("Path");
+        assert_eq!(standard_paths.len(), restricted_paths.len());
+    }
+
+    #[test]
+    fn test_standard_chase_with_existentials() {
+        let instance: Instance = vec![Atom::new("Person", vec![Term::constant("alice")])]
+            .into_iter()
+            .collect();
+
+        let rule = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("HasSSN", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let result = standard_chase(instance, &[rule]);
+
+        assert!(result.terminated);
+        let has_ssn = result.instance.facts_for_predicate("HasSSN");
+        assert_eq!(has_ssn.len(), 1);
+        assert!(matches!(has_ssn[0].terms[1], Term::Null(_)));
+    }
+
+    #[test]
+    fn test_chase_variant_config() {
+        let instance: Instance = vec![Atom::new("A", vec![Term::constant("x")])]
+            .into_iter()
+            .collect();
+
+        let rule = RuleBuilder::new()
+            .when("A", vec![Term::var("X")])
+            .then("B", vec![Term::var("X")])
+            .build();
+
+        // Test standard variant via config
+        let standard_config = ChaseConfig {
+            variant: ChaseVariant::Standard,
+            ..Default::default()
+        };
+        let standard_result = chase_with_config(
+            instance.clone(),
+            std::slice::from_ref(&rule),
+            standard_config,
+        );
+
+        // Test restricted variant via config
+        let restricted_config = ChaseConfig {
+            variant: ChaseVariant::Restricted,
+            ..Default::default()
+        };
+        let restricted_result = chase_with_config(instance, &[rule], restricted_config);
+
+        assert!(standard_result.terminated);
+        assert!(restricted_result.terminated);
+        assert_eq!(
+            standard_result.instance.facts_for_predicate("B").len(),
+            restricted_result.instance.facts_for_predicate("B").len()
+        );
+    }
+
+    // EGD tests
+    use crate::chase::rule::EgdBuilder;
+
+    #[test]
+    fn test_egd_functional_dependency_merges_nulls() {
+        // Functional dependency: R(X, Y), R(X, Z) -> Y = Z
+        // This should merge the nulls created for the same X value
+        let instance: Instance = vec![Atom::new("Person", vec![Term::constant("alice")])]
+            .into_iter()
+            .collect();
+
+        // TGD: Person(X) -> R(X, Y)
+        let tgd = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("R", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        // First run without EGD to create two separate facts with nulls
+        // We simulate this by having two different TGDs create facts
+        let tgd2 = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("S", vec![Term::var("X"), Term::var("Z")])
+            .build();
+
+        // EGD: R(X, Y), S(X, Z) -> Y = Z
+        let egd = EgdBuilder::new()
+            .when("R", vec![Term::var("X"), Term::var("Y")])
+            .when("S", vec![Term::var("X"), Term::var("Z")])
+            .then_equal(Term::var("Y"), Term::var("Z"))
+            .build();
+
+        let result = chase_with_egds(instance, &[tgd, tgd2], &[egd]);
+
+        assert!(result.terminated);
+        assert!(result.error.is_none());
+
+        // After EGD application, the nulls should be merged
+        let r_facts = result.instance.facts_for_predicate("R");
+        let s_facts = result.instance.facts_for_predicate("S");
+        assert_eq!(r_facts.len(), 1);
+        assert_eq!(s_facts.len(), 1);
+
+        // The second argument of R and S should be the same (merged)
+        assert_eq!(r_facts[0].terms[1], s_facts[0].terms[1]);
+    }
+
+    #[test]
+    fn test_egd_conflict_different_constants() {
+        // EGD that tries to equate different constants should fail
+        let instance: Instance = vec![
+            Atom::new("R", vec![Term::constant("x"), Term::constant("alice")]),
+            Atom::new("R", vec![Term::constant("x"), Term::constant("bob")]),
+        ]
+        .into_iter()
+        .collect();
+
+        // EGD: R(X, Y), R(X, Z) -> Y = Z
+        // This should fail because alice != bob
+        let egd = EgdBuilder::new()
+            .when("R", vec![Term::var("X"), Term::var("Y")])
+            .when("R", vec![Term::var("X"), Term::var("Z")])
+            .then_equal(Term::var("Y"), Term::var("Z"))
+            .build();
+
+        let result = chase_with_egds(instance, &[], &[egd]);
+
+        assert!(!result.terminated);
+        assert!(result.error.is_some());
+        assert!(matches!(result.error, Some(ChaseError::EgdConflict(_))));
+    }
+
+    #[test]
+    fn test_egd_null_merged_with_constant() {
+        // EGD that merges a null with a constant
+        let instance: Instance = vec![
+            Atom::new("R", vec![Term::constant("x"), Term::Null(0)]),
+            Atom::new("R", vec![Term::constant("x"), Term::constant("alice")]),
+        ]
+        .into_iter()
+        .collect();
+
+        // EGD: R(X, Y), R(X, Z) -> Y = Z
+        let egd = EgdBuilder::new()
+            .when("R", vec![Term::var("X"), Term::var("Y")])
+            .when("R", vec![Term::var("X"), Term::var("Z")])
+            .then_equal(Term::var("Y"), Term::var("Z"))
+            .build();
+
+        let result = chase_with_egds(instance, &[], &[egd]);
+
+        assert!(result.terminated);
+        assert!(result.error.is_none());
+
+        // After canonicalization, there should be only one R fact
+        // with "alice" as the second argument
+        let r_facts = result.instance.facts_for_predicate("R");
+        assert_eq!(r_facts.len(), 1);
+        assert_eq!(r_facts[0].terms[1], Term::constant("alice"));
+    }
+
+    #[test]
+    fn test_tgd_and_egd_interaction() {
+        // TGD creates facts, EGD enforces constraints
+        let instance: Instance = vec![
+            Atom::new("Person", vec![Term::constant("alice")]),
+            Atom::new("Person", vec![Term::constant("bob")]),
+        ]
+        .into_iter()
+        .collect();
+
+        // TGD: Person(X) -> HasManager(X, Y)
+        let tgd = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("HasManager", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        // EGD: HasManager(X, Y), HasManager(Z, W) -> Y = W
+        // Everyone has the same manager
+        let egd = EgdBuilder::new()
+            .when("HasManager", vec![Term::var("X"), Term::var("Y")])
+            .when("HasManager", vec![Term::var("Z"), Term::var("W")])
+            .then_equal(Term::var("Y"), Term::var("W"))
+            .build();
+
+        let result = chase_with_egds(instance, &[tgd], &[egd]);
+
+        assert!(result.terminated);
+        assert!(result.error.is_none());
+
+        let manager_facts = result.instance.facts_for_predicate("HasManager");
+        assert_eq!(manager_facts.len(), 2);
+
+        // Both should have the same manager (second argument)
+        let managers: Vec<_> = manager_facts.iter().map(|f| &f.terms[1]).collect();
+        assert_eq!(managers[0], managers[1]);
+    }
+
+    #[test]
+    fn test_chase_full_with_custom_config() {
+        let instance: Instance = vec![Atom::new("A", vec![Term::constant("x")])]
+            .into_iter()
+            .collect();
+
+        let tgd = RuleBuilder::new()
+            .when("A", vec![Term::var("X")])
+            .then("B", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let config = ChaseConfig {
+            max_steps: 100,
+            variant: ChaseVariant::Standard,
+        };
+
+        let result = chase_full(instance, &[tgd], &[], config);
+
+        assert!(result.terminated);
+        assert!(result.error.is_none());
+        assert_eq!(result.instance.facts_for_predicate("B").len(), 1);
+    }
+}

src/chase/inference.rs

@@ -0,0 +1,272 @@
+//! Shared reasoning utilities built on top of the chase data model.
+//!
+//! This module keeps query matching and provenance-aware materialization inside
+//! the chase subsystem so frontends do not need to reimplement engine logic.
+
+use std::collections::{HashMap, HashSet};
+
+use super::atom::Atom;
+use super::engine::{ChaseConfig, ChaseResult};
+use super::instance::Instance;
+use super::rule::Rule;
+use super::substitution::{Substitution, unify_atom};
+use super::term::Term;
+
+#[derive(Debug)]
+pub struct MaterializedState {
+    pub result: ChaseResult,
+    provenance: HashMap<Atom, Derivation>,
+}
+
+#[derive(Debug, Clone)]
+pub enum Derivation {
+    Input,
+    Derived {
+        rule_index: usize,
+        rule: Rule,
+        premises: Vec<Atom>,
+    },
+}
+
+#[derive(Debug, Default)]
+pub(crate) struct NullGenerator {
+    counter: usize,
+}
+
+impl NullGenerator {
+    pub(crate) fn seeded_from(instance: &Instance, rules: &[Rule]) -> Self {
+        Self {
+            counter: next_null_id(instance, rules),
+        }
+    }
+
+    pub(crate) fn fresh(&mut self) -> Term {
+        let id = self.counter;
+        self.counter += 1;
+        Term::Null(id)
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub(crate) struct Trigger {
+    rule_index: usize,
+    frontier_bindings: Vec<(String, Term)>,
+}
+
+impl Trigger {
+    pub(crate) fn new(rule_index: usize, rule: &Rule, subst: &Substitution) -> Self {
+        let frontier = rule.frontier_variables();
+        let mut bindings: Vec<_> = frontier
+            .into_iter()
+            .filter_map(|variable| subst.get(&variable).map(|term| (variable, term.clone())))
+            .collect();
+        bindings.sort_by(|left, right| left.0.cmp(&right.0));
+
+        Self {
+            rule_index,
+            frontier_bindings: bindings,
+        }
+    }
+}
+
+#[derive(Debug)]
+struct PendingFact {
+    fact: Atom,
+    derivation: Derivation,
+}
+
+pub fn materialize(base_instance: Instance, rules: &[Rule]) -> MaterializedState {
+    let mut instance = base_instance;
+    let mut provenance = instance
+        .iter()
+        .cloned()
+        .map(|fact| (fact, Derivation::Input))
+        .collect::<HashMap<_, _>>();
+    let max_steps = ChaseConfig::default().max_steps;
+    let mut null_gen = NullGenerator::seeded_from(&instance, rules);
+    let mut applied_triggers = HashSet::new();
+    let mut steps = 0;
+
+    loop {
+        if steps >= max_steps {
+            return MaterializedState {
+                result: ChaseResult {
+                    instance,
+                    steps,
+                    terminated: false,
+                    error: None,
+                },
+                provenance,
+            };
+        }
+
+        let derived = chase_step(
+            &instance,
+            rules,
+            &mut null_gen,
+            &mut applied_triggers,
+            &provenance,
+        );
+
+        if derived.is_empty() {
+            return MaterializedState {
+                result: ChaseResult {
+                    instance,
+                    steps,
+                    terminated: true,
+                    error: None,
+                },
+                provenance,
+            };
+        }
+
+        for pending in derived {
+            if instance.add(pending.fact.clone()) {
+                provenance.entry(pending.fact).or_insert(pending.derivation);
+            }
+        }
+
+        steps += 1;
+    }
+}
+
+pub fn find_matches(instance: &Instance, body: &[Atom]) -> Vec<Substitution> {
+    if body.is_empty() {
+        return vec![Substitution::new()];
+    }
+
+    let mut results = vec![Substitution::new()];
+
+    for body_atom in body {
+        let mut new_results = Vec::new();
+
+        for subst in &results {
+            let pattern = subst.apply_atom(body_atom);
+            for fact in instance.facts_matching_pattern(&pattern) {
+                if let Some(next_subst) = unify_atom(&pattern, fact) {
+                    let mut combined = subst.clone();
+                    for (var, term) in next_subst.iter() {
+                        combined.bind(var.clone(), term.clone());
+                    }
+                    new_results.push(combined);
+                }
+            }
+        }
+
+        results = new_results;
+    }
+
+    results
+}
+
+impl MaterializedState {
+    pub fn provenance_for(&self, atom: &Atom) -> Option<&Derivation> {
+        self.provenance.get(atom)
+    }
+}
+
+pub(crate) fn head_is_satisfied(instance: &Instance, rule: &Rule, subst: &Substitution) -> bool {
+    let head = rule
+        .head
+        .iter()
+        .map(|atom| subst.apply_atom(atom))
+        .collect::<Vec<_>>();
+
+    !find_matches(instance, &head).is_empty()
+}
+
+pub(crate) fn apply_rule_head(
+    rule: &Rule,
+    subst: &Substitution,
+    null_gen: &mut NullGenerator,
+) -> Vec<Atom> {
+    let mut extended_subst = subst.clone();
+    let mut existentials = rule.existential_variables().into_iter().collect::<Vec<_>>();
+    existentials.sort();
+
+    for variable in existentials {
+        extended_subst.bind(variable, null_gen.fresh());
+    }
+
+    rule.head
+        .iter()
+        .map(|atom| extended_subst.apply_atom(atom))
+        .collect()
+}
+
+pub(crate) fn next_null_id(instance: &Instance, rules: &[Rule]) -> usize {
+    let instance_max = instance
+        .iter()
+        .flat_map(|atom| atom.terms.iter())
+        .filter_map(term_null_id)
+        .max();
+    let rule_max = rules
+        .iter()
+        .flat_map(|rule| rule.body.iter().chain(rule.head.iter()))
+        .flat_map(|atom| atom.terms.iter())
+        .filter_map(term_null_id)
+        .max();
+
+    instance_max
+        .into_iter()
+        .chain(rule_max)
+        .max()
+        .map_or(0, |id| id.saturating_add(1))
+}
+
+fn chase_step(
+    instance: &Instance,
+    rules: &[Rule],
+    null_gen: &mut NullGenerator,
+    applied_triggers: &mut HashSet<Trigger>,
+    provenance: &HashMap<Atom, Derivation>,
+) -> Vec<PendingFact> {
+    let mut pending = Vec::new();
+
+    for (rule_index, rule) in rules.iter().enumerate() {
+        let matches = find_matches(instance, &rule.body);
+
+        for subst in matches {
+            let trigger = Trigger::new(rule_index, rule, &subst);
+            if applied_triggers.contains(&trigger) {
+                continue;
+            }
+
+            if head_is_satisfied(instance, rule, &subst) {
+                continue;
+            }
+
+            applied_triggers.insert(trigger);
+
+            let premises = rule
+                .body
+                .iter()
+                .map(|atom| subst.apply_atom(atom))
+                .collect::<Vec<_>>();
+
+            for fact in apply_rule_head(rule, &subst, null_gen) {
+                if instance.contains(&fact) || provenance.contains_key(&fact) {
+                    continue;
+                }
+
+                pending.push(PendingFact {
+                    fact,
+                    derivation: Derivation::Derived {
+                        rule_index: rule_index + 1,
+                        rule: rule.clone(),
+                        premises: premises.clone(),
+                    },
+                });
+            }
+        }
+    }
+
+    pending
+}
+
+fn term_null_id(term: &Term) -> Option<usize> {
+    match term {
+        Term::Null(id) => Some(*id),
+        _ => None,
+    }
+}

src/chase/instance.rs

@@ -0,0 +1,349 @@
+//! A database instance is a set of ground atoms (facts).
+
+use std::collections::{HashMap, HashSet};
+use std::error::Error;
+use std::fmt;
+
+use super::atom::Atom;
+use super::term::Term;
+use super::union_find::UnionFind;
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum InstanceError {
+    NonGroundFact(Atom),
+}
+
+impl fmt::Display for InstanceError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            InstanceError::NonGroundFact(atom) => {
+                write!(f, "facts must be ground atoms: {}", atom)
+            }
+        }
+    }
+}
+
+impl Error for InstanceError {}
+
+/// A key for argument-position indexing: (predicate, position, value).
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+struct IndexKey {
+    predicate: String,
+    position: usize,
+    value: Term,
+}
+
+impl IndexKey {
+    fn new(predicate: &str, position: usize, value: &Term) -> Self {
+        IndexKey {
+            predicate: predicate.to_string(),
+            position,
+            value: value.clone(),
+        }
+    }
+}
+
+/// A database instance containing ground atoms.
+#[derive(Debug, Clone, Default)]
+pub struct Instance {
+    facts_by_predicate: HashMap<String, HashSet<Atom>>,
+    /// Secondary index: maps (predicate, position, value) to atoms with that value at that position.
+    argument_index: HashMap<IndexKey, HashSet<Atom>>,
+    len: usize,
+}
+
+impl Instance {
+    /// Create an empty instance.
+    pub fn new() -> Self {
+        Instance {
+            facts_by_predicate: HashMap::new(),
+            argument_index: HashMap::new(),
+            len: 0,
+        }
+    }
+
+    /// Try to add a fact to the instance. Returns true if the fact was new.
+    pub fn try_add(&mut self, fact: Atom) -> Result<bool, InstanceError> {
+        if !fact.is_ground() {
+            return Err(InstanceError::NonGroundFact(fact));
+        }
+
+        let bucket = self
+            .facts_by_predicate
+            .entry(fact.predicate.clone())
+            .or_default();
+        let inserted = bucket.insert(fact.clone());
+        if inserted {
+            // Populate argument indexes
+            for (position, term) in fact.terms.iter().enumerate() {
+                let key = IndexKey::new(&fact.predicate, position, term);
+                self.argument_index
+                    .entry(key)
+                    .or_default()
+                    .insert(fact.clone());
+            }
+            self.len += 1;
+        }
+
+        Ok(inserted)
+    }
+
+    /// Add a fact to the instance. Returns true if the fact was new.
+    ///
+    /// # Panics
+    /// Panics if the atom is not ground.
+    #[allow(clippy::expect_used)]
+    pub fn add(&mut self, fact: Atom) -> bool {
+        self.try_add(fact).expect("facts must be ground atoms")
+    }
+
+    /// Check if the instance contains a fact.
+    pub fn contains(&self, fact: &Atom) -> bool {
+        self.facts_by_predicate
+            .get(&fact.predicate)
+            .is_some_and(|facts| facts.contains(fact))
+    }
+
+    /// Get the number of facts.
+    pub fn len(&self) -> usize {
+        self.len
+    }
+
+    /// Check if the instance is empty.
+    pub fn is_empty(&self) -> bool {
+        self.len == 0
+    }
+
+    /// Iterate over all facts.
+    pub fn iter(&self) -> impl Iterator<Item = &Atom> {
+        self.facts_by_predicate
+            .values()
+            .flat_map(|facts| facts.iter())
+    }
+
+    /// Get all facts with a given predicate.
+    pub fn facts_for_predicate(&self, predicate: &str) -> Vec<&Atom> {
+        self.facts_by_predicate
+            .get(predicate)
+            .into_iter()
+            .flat_map(|facts| facts.iter())
+            .collect()
+    }
+
+    /// Get facts matching a pattern, using argument indexes for efficient lookup.
+    ///
+    /// The pattern may contain variables (which match anything) and ground terms
+    /// (which must match exactly). This method uses a selectivity heuristic to
+    /// choose the most selective index for lookup.
+    pub fn facts_matching_pattern(&self, pattern: &Atom) -> Vec<&Atom> {
+        // Find bound (ground) positions and their selectivity
+        let bound_positions: Vec<(usize, &Term)> = pattern
+            .terms
+            .iter()
+            .enumerate()
+            .filter(|(_, term)| term.is_ground())
+            .collect();
+
+        if bound_positions.is_empty() {
+            // No bound arguments, fall back to predicate lookup
+            return self.facts_for_predicate(&pattern.predicate);
+        }
+
+        // Use selectivity heuristic: pick the bound position with the smallest bucket
+        let mut best_key: Option<IndexKey> = None;
+        let mut best_size = usize::MAX;
+
+        for (position, term) in &bound_positions {
+            let key = IndexKey::new(&pattern.predicate, *position, term);
+            let size = self.argument_index.get(&key).map(|s| s.len()).unwrap_or(0);
+
+            if size < best_size {
+                best_size = size;
+                best_key = Some(key);
+            }
+        }
+
+        // If best bucket is empty, return empty
+        let Some(key) = best_key else {
+            return Vec::new();
+        };
+
+        let Some(candidates) = self.argument_index.get(&key) else {
+            return Vec::new();
+        };
+
+        // Filter candidates by arity and all other bound positions
+        let pattern_arity = pattern.arity();
+        candidates
+            .iter()
+            .filter(|fact| {
+                fact.arity() == pattern_arity
+                    && bound_positions
+                        .iter()
+                        .all(|(pos, term)| &fact.terms[*pos] == *term)
+            })
+            .collect()
+    }
+
+    /// Create a new instance with all atoms canonicalized according to the union-find.
+    ///
+    /// This replaces all nulls with their canonical representatives and removes
+    /// duplicate atoms that result from canonicalization.
+    pub fn canonicalize(&self, uf: &mut UnionFind) -> Instance {
+        let mut new_instance = Instance::new();
+        for atom in self.iter() {
+            let canonical = uf.canonicalize_atom(atom);
+            // try_add handles deduplication
+            let _ = new_instance.try_add(canonical);
+        }
+        new_instance
+    }
+}
+
+impl fmt::Display for Instance {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        writeln!(f, "Instance {{")?;
+        for fact in self.iter() {
+            writeln!(f, "  {}", fact)?;
+        }
+        write!(f, "}}")
+    }
+}
+
+impl FromIterator<Atom> for Instance {
+    fn from_iter<T: IntoIterator<Item = Atom>>(iter: T) -> Self {
+        let mut instance = Instance::new();
+        for atom in iter {
+            instance.add(atom);
+        }
+        instance
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::chase::term::Term;
+
+    #[test]
+    fn test_instance_operations() {
+        let mut instance = Instance::new();
+
+        let fact1 = Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        );
+        let fact2 = Atom::new(
+            "Parent",
+            vec![Term::constant("bob"), Term::constant("carol")],
+        );
+
+        assert!(instance.add(fact1.clone()));
+        assert!(instance.add(fact2.clone()));
+        assert!(!instance.add(fact1.clone())); // Duplicate
+
+        assert_eq!(instance.len(), 2);
+        assert!(instance.contains(&fact1));
+    }
+
+    #[test]
+    fn test_facts_for_predicate() {
+        let instance: Instance = vec![
+            Atom::new(
+                "Parent",
+                vec![Term::constant("alice"), Term::constant("bob")],
+            ),
+            Atom::new("Person", vec![Term::constant("alice")]),
+        ]
+        .into_iter()
+        .collect();
+
+        assert_eq!(instance.facts_for_predicate("Parent").len(), 1);
+        assert_eq!(instance.facts_for_predicate("Person").len(), 1);
+        assert_eq!(instance.facts_for_predicate("Other").len(), 0);
+    }
+
+    #[test]
+    fn test_try_add_rejects_non_ground_facts() {
+        let mut instance = Instance::new();
+        let fact = Atom::new("Parent", vec![Term::var("X"), Term::constant("bob")]);
+
+        let error = instance.try_add(fact).unwrap_err();
+
+        assert!(matches!(error, InstanceError::NonGroundFact(_)));
+        assert!(instance.is_empty());
+    }
+
+    #[test]
+    fn test_facts_matching_pattern_with_bound_arg() {
+        let instance: Instance = vec![
+            Atom::new(
+                "Parent",
+                vec![Term::constant("alice"), Term::constant("bob")],
+            ),
+            Atom::new(
+                "Parent",
+                vec![Term::constant("alice"), Term::constant("carol")],
+            ),
+            Atom::new(
+                "Parent",
+                vec![Term::constant("bob"), Term::constant("carol")],
+            ),
+        ]
+        .into_iter()
+        .collect();
+
+        // Pattern with first argument bound to "alice"
+        let pattern = Atom::new("Parent", vec![Term::constant("alice"), Term::var("Y")]);
+        let matches = instance.facts_matching_pattern(&pattern);
+        assert_eq!(matches.len(), 2);
+
+        // Pattern with second argument bound to "carol"
+        let pattern = Atom::new("Parent", vec![Term::var("X"), Term::constant("carol")]);
+        let matches = instance.facts_matching_pattern(&pattern);
+        assert_eq!(matches.len(), 2);
+
+        // Pattern with both arguments bound
+        let pattern = Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        );
+        let matches = instance.facts_matching_pattern(&pattern);
+        assert_eq!(matches.len(), 1);
+
+        // Pattern with no bound arguments (all variables)
+        let pattern = Atom::new("Parent", vec![Term::var("X"), Term::var("Y")]);
+        let matches = instance.facts_matching_pattern(&pattern);
+        assert_eq!(matches.len(), 3);
+
+        // Pattern with non-matching bound argument
+        let pattern = Atom::new("Parent", vec![Term::constant("dave"), Term::var("Y")]);
+        let matches = instance.facts_matching_pattern(&pattern);
+        assert_eq!(matches.len(), 0);
+    }
+
+    #[test]
+    fn test_facts_matching_pattern_selectivity() {
+        // Create instance with skewed distribution
+        let mut instance = Instance::new();
+
+        // Many facts with first arg "common"
+        for i in 0..100 {
+            instance.add(Atom::new(
+                "R",
+                vec![Term::constant("common"), Term::constant(format!("v{}", i))],
+            ));
+        }
+        // One fact with first arg "rare"
+        instance.add(Atom::new(
+            "R",
+            vec![Term::constant("rare"), Term::constant("x")],
+        ));
+
+        // Pattern matching on "rare" should use more selective index
+        let pattern = Atom::new("R", vec![Term::constant("rare"), Term::var("Y")]);
+        let matches = instance.facts_matching_pattern(&pattern);
+        assert_eq!(matches.len(), 1);
+        assert_eq!(matches[0].terms[0], Term::constant("rare"));
+    }
+}

src/chase/mod.rs

@@ -0,0 +1,23 @@
+//! Chase algorithm implementation for reasoning with tuple-generating dependencies (TGDs).
+
+pub mod atom;
+pub mod inference;
+pub mod instance;
+pub mod rule;
+pub mod substitution;
+pub mod term;
+pub mod union_find;
+
+mod engine;
+
+pub use atom::Atom;
+pub use engine::{
+    ChaseConfig, ChaseError, ChaseResult, ChaseVariant, chase, chase_full, chase_with_config,
+    chase_with_egds, standard_chase,
+};
+pub use inference::{Derivation, MaterializedState, find_matches, materialize};
+pub use instance::{Instance, InstanceError};
+pub use rule::{Egd, EgdBuilder, Equality, Rule, RuleBuilder};
+pub use substitution::Substitution;
+pub use term::Term;
+pub use union_find::{MergeError, UnionFind};

src/chase/rule.rs

@@ -0,0 +1,289 @@
+//! Rules (tuple-generating dependencies / TGDs) for the chase.
+
+use std::collections::HashSet;
+use std::fmt;
+
+use super::atom::Atom;
+use super::term::Term;
+
+/// A rule (TGD) of the form: body -> head
+///
+/// The body is a conjunction of atoms, and the head is a conjunction of atoms.
+/// Variables in the head that don't appear in the body are "existential" -
+/// they will be replaced with fresh nulls during the chase.
+#[derive(Debug, Clone)]
+pub struct Rule {
+    /// The body atoms (conjunction).
+    pub body: Vec<Atom>,
+    /// The head atoms (conjunction).
+    pub head: Vec<Atom>,
+}
+
+impl Rule {
+    /// Create a new rule.
+    pub fn new(body: Vec<Atom>, head: Vec<Atom>) -> Self {
+        Rule { body, head }
+    }
+
+    /// Get all variables appearing in the body.
+    pub fn body_variables(&self) -> HashSet<String> {
+        self.body
+            .iter()
+            .flat_map(|a| a.variables())
+            .cloned()
+            .collect()
+    }
+
+    /// Get all variables appearing in the head.
+    pub fn head_variables(&self) -> HashSet<String> {
+        self.head
+            .iter()
+            .flat_map(|a| a.variables())
+            .cloned()
+            .collect()
+    }
+
+    /// Get existentially quantified variables (in head but not in body).
+    pub fn existential_variables(&self) -> HashSet<String> {
+        let body_vars = self.body_variables();
+        self.head_variables()
+            .into_iter()
+            .filter(|v| !body_vars.contains(v))
+            .collect()
+    }
+
+    /// Get frontier variables (in both body and head).
+    pub fn frontier_variables(&self) -> HashSet<String> {
+        let body_vars = self.body_variables();
+        self.head_variables()
+            .into_iter()
+            .filter(|v| body_vars.contains(v))
+            .collect()
+    }
+}
+
+impl fmt::Display for Rule {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        // Body
+        for (i, atom) in self.body.iter().enumerate() {
+            if i > 0 {
+                write!(f, ", ")?;
+            }
+            write!(f, "{}", atom)?;
+        }
+        write!(f, " → ")?;
+        // Head
+        for (i, atom) in self.head.iter().enumerate() {
+            if i > 0 {
+                write!(f, ", ")?;
+            }
+            write!(f, "{}", atom)?;
+        }
+        Ok(())
+    }
+}
+
+/// Builder for creating rules with a fluent API.
+pub struct RuleBuilder {
+    body: Vec<Atom>,
+    head: Vec<Atom>,
+}
+
+impl RuleBuilder {
+    pub fn new() -> Self {
+        RuleBuilder {
+            body: Vec::new(),
+            head: Vec::new(),
+        }
+    }
+
+    /// Add an atom to the body.
+    pub fn when(mut self, predicate: &str, terms: Vec<Term>) -> Self {
+        self.body.push(Atom::new(predicate, terms));
+        self
+    }
+
+    /// Add an atom to the head.
+    pub fn then(mut self, predicate: &str, terms: Vec<Term>) -> Self {
+        self.head.push(Atom::new(predicate, terms));
+        self
+    }
+
+    /// Build the rule.
+    pub fn build(self) -> Rule {
+        Rule::new(self.body, self.head)
+    }
+}
+
+impl Default for RuleBuilder {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// An equality constraint between two terms.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Equality {
+    pub left: Term,
+    pub right: Term,
+}
+
+impl Equality {
+    /// Create a new equality constraint.
+    pub fn new(left: Term, right: Term) -> Self {
+        Equality { left, right }
+    }
+
+    /// Get all variables in this equality.
+    pub fn variables(&self) -> Vec<&String> {
+        let mut vars = Vec::new();
+        if let Term::Variable(v) = &self.left {
+            vars.push(v);
+        }
+        if let Term::Variable(v) = &self.right {
+            vars.push(v);
+        }
+        vars
+    }
+}
+
+impl fmt::Display for Equality {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{} = {}", self.left, self.right)
+    }
+}
+
+/// An equality-generating dependency (EGD).
+///
+/// EGDs have the form: body -> X = Y
+/// When the body matches, the equality X = Y is enforced.
+#[derive(Debug, Clone)]
+pub struct Egd {
+    /// The body atoms (conjunction).
+    pub body: Vec<Atom>,
+    /// The equality to enforce.
+    pub equality: Equality,
+}
+
+impl Egd {
+    /// Create a new EGD.
+    pub fn new(body: Vec<Atom>, equality: Equality) -> Self {
+        Egd { body, equality }
+    }
+
+    /// Get all variables appearing in the body.
+    pub fn body_variables(&self) -> HashSet<String> {
+        self.body
+            .iter()
+            .flat_map(|a| a.variables())
+            .cloned()
+            .collect()
+    }
+
+    /// Get all variables appearing in the equality.
+    pub fn equality_variables(&self) -> HashSet<String> {
+        self.equality.variables().into_iter().cloned().collect()
+    }
+}
+
+impl fmt::Display for Egd {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        for (i, atom) in self.body.iter().enumerate() {
+            if i > 0 {
+                write!(f, ", ")?;
+            }
+            write!(f, "{}", atom)?;
+        }
+        write!(f, " → {}", self.equality)
+    }
+}
+
+/// Builder for creating EGDs with a fluent API.
+pub struct EgdBuilder {
+    body: Vec<Atom>,
+    equality: Option<Equality>,
+}
+
+impl EgdBuilder {
+    pub fn new() -> Self {
+        EgdBuilder {
+            body: Vec::new(),
+            equality: None,
+        }
+    }
+
+    /// Add an atom to the body.
+    pub fn when(mut self, predicate: &str, terms: Vec<Term>) -> Self {
+        self.body.push(Atom::new(predicate, terms));
+        self
+    }
+
+    /// Set the equality to enforce.
+    pub fn then_equal(mut self, left: Term, right: Term) -> Self {
+        self.equality = Some(Equality::new(left, right));
+        self
+    }
+
+    /// Build the EGD.
+    ///
+    /// # Panics
+    /// Panics if `then_equal()` was not called.
+    #[allow(clippy::expect_used)]
+    pub fn build(self) -> Egd {
+        Egd::new(self.body, self.equality.expect("EGD must have an equality"))
+    }
+}
+
+impl Default for EgdBuilder {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_rule_variables() {
+        // Parent(X, Y), Parent(Y, Z) -> Grandparent(X, Z)
+        let rule = RuleBuilder::new()
+            .when("Parent", vec![Term::var("X"), Term::var("Y")])
+            .when("Parent", vec![Term::var("Y"), Term::var("Z")])
+            .then("Grandparent", vec![Term::var("X"), Term::var("Z")])
+            .build();
+
+        let body_vars = rule.body_variables();
+        assert!(body_vars.contains("X"));
+        assert!(body_vars.contains("Y"));
+        assert!(body_vars.contains("Z"));
+
+        assert!(rule.existential_variables().is_empty());
+    }
+
+    #[test]
+    fn test_existential_variables() {
+        // Person(X) -> HasId(X, Y) where Y is existential
+        let rule = RuleBuilder::new()
+            .when("Person", vec![Term::var("X")])
+            .then("HasId", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let existential = rule.existential_variables();
+        assert!(existential.contains("Y"));
+        assert!(!existential.contains("X"));
+    }
+
+    #[test]
+    fn test_rule_display() {
+        let rule = RuleBuilder::new()
+            .when("Parent", vec![Term::var("X"), Term::var("Y")])
+            .then("Ancestor", vec![Term::var("X"), Term::var("Y")])
+            .build();
+
+        let display = format!("{}", rule);
+        assert!(display.contains("Parent"));
+        assert!(display.contains("Ancestor"));
+        assert!(display.contains("→"));
+    }
+}

src/chase/substitution.rs

@@ -0,0 +1,147 @@
+//! Substitutions map variables to terms.
+
+use std::collections::HashMap;
+
+use super::atom::Atom;
+use super::term::Term;
+
+/// A substitution maps variable names to terms.
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+pub struct Substitution {
+    mapping: HashMap<String, Term>,
+}
+
+impl Substitution {
+    /// Create an empty substitution.
+    pub fn new() -> Self {
+        Substitution {
+            mapping: HashMap::new(),
+        }
+    }
+
+    /// Bind a variable to a term.
+    pub fn bind(&mut self, var: String, term: Term) {
+        self.mapping.insert(var, term);
+    }
+
+    /// Get the term bound to a variable, if any.
+    pub fn get(&self, var: &str) -> Option<&Term> {
+        self.mapping.get(var)
+    }
+
+    /// Apply this substitution to a term.
+    pub fn apply_term(&self, term: &Term) -> Term {
+        match term {
+            Term::Variable(v) => self.mapping.get(v).cloned().unwrap_or_else(|| term.clone()),
+            _ => term.clone(),
+        }
+    }
+
+    /// Apply this substitution to an atom.
+    pub fn apply_atom(&self, atom: &Atom) -> Atom {
+        Atom::new(
+            atom.predicate.clone(),
+            atom.terms.iter().map(|t| self.apply_term(t)).collect(),
+        )
+    }
+
+    /// Check if this substitution is empty.
+    pub fn is_empty(&self) -> bool {
+        self.mapping.is_empty()
+    }
+
+    /// Get the number of bindings.
+    pub fn len(&self) -> usize {
+        self.mapping.len()
+    }
+
+    /// Iterate over all bindings.
+    pub fn iter(&self) -> impl Iterator<Item = (&String, &Term)> {
+        self.mapping.iter()
+    }
+}
+
+/// Try to unify an atom pattern with a ground atom (fact).
+/// Returns Some(substitution) if they unify, None otherwise.
+pub fn unify_atom(pattern: &Atom, fact: &Atom) -> Option<Substitution> {
+    if pattern.predicate != fact.predicate || pattern.arity() != fact.arity() {
+        return None;
+    }
+
+    let mut subst = Substitution::new();
+
+    for (pattern_term, fact_term) in pattern.terms.iter().zip(fact.terms.iter()) {
+        match pattern_term {
+            Term::Variable(v) => {
+                if let Some(existing) = subst.get(v) {
+                    if existing != fact_term {
+                        return None; // Conflict
+                    }
+                } else {
+                    subst.bind(v.clone(), fact_term.clone());
+                }
+            }
+            Term::Constant(c1) => {
+                if let Term::Constant(c2) = fact_term {
+                    if c1 != c2 {
+                        return None;
+                    }
+                } else {
+                    return None;
+                }
+            }
+            Term::Null(n1) => {
+                if let Term::Null(n2) = fact_term {
+                    if n1 != n2 {
+                        return None;
+                    }
+                } else {
+                    return None;
+                }
+            }
+        }
+    }
+
+    Some(subst)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_substitution_apply() {
+        let mut subst = Substitution::new();
+        subst.bind("X".to_string(), Term::constant("alice"));
+        subst.bind("Y".to_string(), Term::constant("bob"));
+
+        let atom = Atom::new("Parent", vec![Term::var("X"), Term::var("Y")]);
+        let result = subst.apply_atom(&atom);
+
+        assert!(result.is_ground());
+        assert_eq!(format!("{}", result), "Parent(alice, bob)");
+    }
+
+    #[test]
+    fn test_unify_success() {
+        let pattern = Atom::new("Parent", vec![Term::var("X"), Term::constant("bob")]);
+        let fact = Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        );
+
+        let subst = unify_atom(&pattern, &fact).unwrap();
+        assert_eq!(subst.get("X"), Some(&Term::constant("alice")));
+    }
+
+    #[test]
+    fn test_unify_failure() {
+        let pattern = Atom::new("Parent", vec![Term::var("X"), Term::constant("carol")]);
+        let fact = Atom::new(
+            "Parent",
+            vec![Term::constant("alice"), Term::constant("bob")],
+        );
+
+        assert!(unify_atom(&pattern, &fact).is_none());
+    }
+}

src/chase/term.rs

@@ -0,0 +1,105 @@
+//! Terms represent values in the chase: constants or labeled nulls.
+
+use std::fmt;
+
+/// A term is either a constant (from the input) or a null (invented during chase).
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum Term {
+    /// A constant value from the domain.
+    Constant(String),
+    /// A labeled null (invented value) created during the chase.
+    /// The usize is a unique identifier for this null.
+    Null(usize),
+    /// A variable (used in rule bodies/heads, not in instances).
+    Variable(String),
+}
+
+impl Term {
+    /// Create a new constant term.
+    pub fn constant(value: impl Into<String>) -> Self {
+        Term::Constant(value.into())
+    }
+
+    /// Create a new null term with the given id.
+    pub fn null(id: usize) -> Self {
+        Term::Null(id)
+    }
+
+    /// Create a new variable term.
+    pub fn var(name: impl Into<String>) -> Self {
+        Term::Variable(name.into())
+    }
+
+    /// Returns true if this term is a variable.
+    pub fn is_variable(&self) -> bool {
+        matches!(self, Term::Variable(_))
+    }
+
+    /// Returns true if this term is ground (not a variable).
+    pub fn is_ground(&self) -> bool {
+        !self.is_variable()
+    }
+
+    /// Returns true if this term is a null.
+    pub fn is_null(&self) -> bool {
+        matches!(self, Term::Null(_))
+    }
+
+    /// Returns true if this term is a constant.
+    pub fn is_constant(&self) -> bool {
+        matches!(self, Term::Constant(_))
+    }
+}
+
+impl fmt::Display for Term {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Term::Constant(c) => write!(f, "{}", c),
+            Term::Null(id) => write!(f, "⊥{}", id),
+            Term::Variable(v) => write!(f, "?{}", v),
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_term_creation() {
+        let c = Term::constant("alice");
+        let n = Term::null(1);
+        let v = Term::var("X");
+
+        assert!(matches!(c, Term::Constant(_)));
+        assert!(matches!(n, Term::Null(1)));
+        assert!(matches!(v, Term::Variable(_)));
+    }
+
+    #[test]
+    fn test_term_properties() {
+        let c = Term::constant("alice");
+        let v = Term::var("X");
+
+        assert!(c.is_ground());
+        assert!(!c.is_variable());
+        assert!(!v.is_ground());
+        assert!(v.is_variable());
+    }
+
+    #[test]
+    fn test_is_null_and_is_constant() {
+        let c = Term::constant("alice");
+        let n = Term::null(1);
+        let v = Term::var("X");
+
+        assert!(c.is_constant());
+        assert!(!c.is_null());
+
+        assert!(n.is_null());
+        assert!(!n.is_constant());
+
+        assert!(!v.is_constant());
+        assert!(!v.is_null());
+    }
+}

src/chase/union_find.rs

@@ -0,0 +1,323 @@
+//! Union-Find data structure for managing null equivalence classes in EGDs.
+
+use std::collections::HashMap;
+use std::error::Error;
+use std::fmt;
+
+use super::atom::Atom;
+use super::term::Term;
+
+/// Error that occurs when merging two different constants.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct MergeError {
+    pub left: Term,
+    pub right: Term,
+}
+
+impl fmt::Display for MergeError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            f,
+            "cannot merge different constants: {} and {}",
+            self.left, self.right
+        )
+    }
+}
+
+impl Error for MergeError {}
+
+/// Union-Find data structure for managing equivalence classes of terms.
+///
+/// Used by EGDs to track which nulls have been merged and what their
+/// canonical representatives are. Constants are always their own canonical
+/// form, and merging a null with a constant makes the constant the canonical
+/// form for that equivalence class.
+#[derive(Debug, Clone, Default)]
+pub struct UnionFind {
+    /// Maps null IDs to their parent in the union-find tree.
+    parent: HashMap<usize, usize>,
+    /// Rank for union-by-rank optimization.
+    rank: HashMap<usize, usize>,
+    /// Maps null IDs to their canonical term (constant if merged with one).
+    canonical: HashMap<usize, Term>,
+}
+
+impl UnionFind {
+    /// Create a new empty union-find structure.
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    /// Find the representative for a null ID, with path compression.
+    pub fn find(&mut self, null_id: usize) -> usize {
+        // Ensure the null exists in our structure and get the parent
+        let parent = *self.parent.entry(null_id).or_insert_with(|| {
+            self.rank.insert(null_id, 0);
+            null_id
+        });
+
+        if parent != null_id {
+            // Path compression: make this node point directly to the root
+            let root = self.find(parent);
+            self.parent.insert(null_id, root);
+            root
+        } else {
+            null_id
+        }
+    }
+
+    /// Get the canonical term for a given term.
+    ///
+    /// - Constants are always their own canonical form.
+    /// - Variables are always their own canonical form (shouldn't appear in instances).
+    /// - Nulls are mapped to their canonical representative (which may be a constant
+    ///   if they were merged with one).
+    pub fn canonical_term(&mut self, term: &Term) -> Term {
+        match term {
+            Term::Constant(_) | Term::Variable(_) => term.clone(),
+            Term::Null(id) => {
+                let root = self.find(*id);
+                // Check if this equivalence class has a canonical constant
+                if let Some(canonical) = self.canonical.get(&root) {
+                    canonical.clone()
+                } else {
+                    Term::Null(root)
+                }
+            }
+        }
+    }
+
+    /// Canonicalize an atom by replacing all terms with their canonical forms.
+    pub fn canonicalize_atom(&mut self, atom: &Atom) -> Atom {
+        Atom::new(
+            atom.predicate.clone(),
+            atom.terms.iter().map(|t| self.canonical_term(t)).collect(),
+        )
+    }
+
+    /// Merge two terms, returning an error if they are different constants.
+    ///
+    /// The merge rules are:
+    /// - Null + Null: union the equivalence classes
+    /// - Null + Constant: the constant becomes the canonical form for the null's class
+    /// - Constant + Constant: error if different, no-op if same
+    pub fn merge(&mut self, left: &Term, right: &Term) -> Result<(), MergeError> {
+        match (left, right) {
+            (Term::Constant(c1), Term::Constant(c2)) => {
+                if c1 != c2 {
+                    Err(MergeError {
+                        left: left.clone(),
+                        right: right.clone(),
+                    })
+                } else {
+                    Ok(())
+                }
+            }
+            (Term::Null(id), Term::Constant(_)) => {
+                let root = self.find(*id);
+                // Check if this class already has a canonical constant
+                if let Some(existing) = self.canonical.get(&root) {
+                    if existing != right {
+                        return Err(MergeError {
+                            left: existing.clone(),
+                            right: right.clone(),
+                        });
+                    }
+                } else {
+                    self.canonical.insert(root, right.clone());
+                }
+                Ok(())
+            }
+            (Term::Constant(_), Term::Null(id)) => {
+                let root = self.find(*id);
+                if let Some(existing) = self.canonical.get(&root) {
+                    if existing != left {
+                        return Err(MergeError {
+                            left: left.clone(),
+                            right: existing.clone(),
+                        });
+                    }
+                } else {
+                    self.canonical.insert(root, left.clone());
+                }
+                Ok(())
+            }
+            (Term::Null(id1), Term::Null(id2)) => {
+                let root1 = self.find(*id1);
+                let root2 = self.find(*id2);
+
+                if root1 == root2 {
+                    return Ok(()); // Already in the same class
+                }
+
+                // Check if both have canonical constants
+                let canon1 = self.canonical.get(&root1).cloned();
+                let canon2 = self.canonical.get(&root2).cloned();
+
+                match (&canon1, &canon2) {
+                    (Some(c1), Some(c2)) if c1 != c2 => {
+                        return Err(MergeError {
+                            left: c1.clone(),
+                            right: c2.clone(),
+                        });
+                    }
+                    _ => {}
+                }
+
+                // Union by rank
+                let rank1 = *self.rank.get(&root1).unwrap_or(&0);
+                let rank2 = *self.rank.get(&root2).unwrap_or(&0);
+
+                let (new_root, child) = if rank1 < rank2 {
+                    (root2, root1)
+                } else if rank1 > rank2 {
+                    (root1, root2)
+                } else {
+                    self.rank.insert(root1, rank1 + 1);
+                    (root1, root2)
+                };
+
+                self.parent.insert(child, new_root);
+
+                // Propagate canonical constant to new root
+                let canonical = canon1.or(canon2);
+                if let Some(c) = canonical {
+                    self.canonical.insert(new_root, c);
+                }
+
+                Ok(())
+            }
+            // Variables shouldn't be merged (they shouldn't appear in instances)
+            (Term::Variable(_), _) | (_, Term::Variable(_)) => Ok(()),
+        }
+    }
+
+    /// Check if two terms are in the same equivalence class.
+    pub fn are_equivalent(&mut self, left: &Term, right: &Term) -> bool {
+        self.canonical_term(left) == self.canonical_term(right)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_merge_nulls() {
+        let mut uf = UnionFind::new();
+
+        // Merge two nulls
+        uf.merge(&Term::Null(0), &Term::Null(1)).unwrap();
+
+        // They should now have the same canonical form
+        let canon0 = uf.canonical_term(&Term::Null(0));
+        let canon1 = uf.canonical_term(&Term::Null(1));
+        assert_eq!(canon0, canon1);
+    }
+
+    #[test]
+    fn test_merge_null_with_constant() {
+        let mut uf = UnionFind::new();
+
+        // Merge null with constant
+        uf.merge(&Term::Null(0), &Term::constant("alice")).unwrap();
+
+        // Null should now have the constant as canonical form
+        assert_eq!(uf.canonical_term(&Term::Null(0)), Term::constant("alice"));
+    }
+
+    #[test]
+    fn test_merge_transitive() {
+        let mut uf = UnionFind::new();
+
+        // Merge: null0 = null1, null1 = constant
+        uf.merge(&Term::Null(0), &Term::Null(1)).unwrap();
+        uf.merge(&Term::Null(1), &Term::constant("bob")).unwrap();
+
+        // Both nulls should have the constant as canonical
+        assert_eq!(uf.canonical_term(&Term::Null(0)), Term::constant("bob"));
+        assert_eq!(uf.canonical_term(&Term::Null(1)), Term::constant("bob"));
+    }
+
+    #[test]
+    fn test_merge_different_constants_fails() {
+        let mut uf = UnionFind::new();
+
+        // Merging different constants should fail
+        let result = uf.merge(&Term::constant("alice"), &Term::constant("bob"));
+        assert!(result.is_err());
+
+        let err = result.unwrap_err();
+        assert_eq!(err.left, Term::constant("alice"));
+        assert_eq!(err.right, Term::constant("bob"));
+    }
+
+    #[test]
+    fn test_merge_same_constant_ok() {
+        let mut uf = UnionFind::new();
+
+        // Merging the same constant should be fine
+        uf.merge(&Term::constant("alice"), &Term::constant("alice"))
+            .unwrap();
+    }
+
+    #[test]
+    fn test_merge_nulls_with_conflicting_constants() {
+        let mut uf = UnionFind::new();
+
+        // null0 = alice, null1 = bob
+        uf.merge(&Term::Null(0), &Term::constant("alice")).unwrap();
+        uf.merge(&Term::Null(1), &Term::constant("bob")).unwrap();
+
+        // Merging null0 and null1 should fail (alice != bob)
+        let result = uf.merge(&Term::Null(0), &Term::Null(1));
+        assert!(result.is_err());
+    }
+
+    #[test]
+    fn test_canonicalize_atom() {
+        let mut uf = UnionFind::new();
+
+        uf.merge(&Term::Null(0), &Term::constant("alice")).unwrap();
+        uf.merge(&Term::Null(1), &Term::Null(2)).unwrap();
+
+        let atom = Atom::new("R", vec![Term::Null(0), Term::Null(1), Term::constant("x")]);
+
+        let canonical = uf.canonicalize_atom(&atom);
+
+        assert_eq!(canonical.terms[0], Term::constant("alice"));
+        // Null(1) and Null(2) are equivalent but have no constant, so canonical is one of them
+        assert!(canonical.terms[1].is_null());
+        assert_eq!(canonical.terms[2], Term::constant("x"));
+    }
+
+    #[test]
+    fn test_path_compression() {
+        let mut uf = UnionFind::new();
+
+        // Create a chain: 0 -> 1 -> 2 -> 3
+        uf.merge(&Term::Null(0), &Term::Null(1)).unwrap();
+        uf.merge(&Term::Null(1), &Term::Null(2)).unwrap();
+        uf.merge(&Term::Null(2), &Term::Null(3)).unwrap();
+
+        // Finding from 0 should compress the path
+        let root = uf.find(0);
+
+        // All should point to the same root
+        assert_eq!(uf.find(1), root);
+        assert_eq!(uf.find(2), root);
+        assert_eq!(uf.find(3), root);
+    }
+
+    #[test]
+    fn test_are_equivalent() {
+        let mut uf = UnionFind::new();
+
+        uf.merge(&Term::Null(0), &Term::Null(1)).unwrap();
+
+        assert!(uf.are_equivalent(&Term::Null(0), &Term::Null(1)));
+        assert!(!uf.are_equivalent(&Term::Null(0), &Term::Null(2)));
+        assert!(uf.are_equivalent(&Term::constant("a"), &Term::constant("a")));
+        assert!(!uf.are_equivalent(&Term::constant("a"), &Term::constant("b")));
+    }
+}

src/frontend/language.rs

@@ -0,0 +1,393 @@
+//! Minimal command language for the query-engine REPL and GUI.
+
+use crate::chase::rule::RuleBuilder;
+use crate::chase::{Atom, Rule, Term};
+
+#[derive(Debug, Clone)]
+pub enum Command {
+    Fact(Atom),
+    Rule(Rule),
+    Run,
+    Query(Vec<Atom>),
+    Explain(Vec<Atom>),
+    ShowFacts,
+    ShowRules,
+    Reset,
+    Help,
+}
+
+pub fn parse_script(input: &str) -> Result<Vec<Command>, String> {
+    let mut commands = Vec::new();
+
+    for (index, raw_line) in input.lines().enumerate() {
+        let line = raw_line.trim();
+        if line.is_empty() || line.starts_with('#') {
+            continue;
+        }
+
+        let command = parse_command(line).map_err(|err| format!("line {}: {}", index + 1, err))?;
+        commands.push(command);
+    }
+
+    Ok(commands)
+}
+
+pub fn parse_command(input: &str) -> Result<Command, String> {
+    let trimmed = input.trim();
+
+    if trimmed.eq_ignore_ascii_case("run") || trimmed.eq_ignore_ascii_case("run.") {
+        return Ok(Command::Run);
+    }
+    if trimmed.eq_ignore_ascii_case("show facts") || trimmed.eq_ignore_ascii_case("show facts.") {
+        return Ok(Command::ShowFacts);
+    }
+    if trimmed.eq_ignore_ascii_case("show rules") || trimmed.eq_ignore_ascii_case("show rules.") {
+        return Ok(Command::ShowRules);
+    }
+    if trimmed.eq_ignore_ascii_case("reset") || trimmed.eq_ignore_ascii_case("reset.") {
+        return Ok(Command::Reset);
+    }
+    if trimmed.eq_ignore_ascii_case("help") || trimmed.eq_ignore_ascii_case("help.") {
+        return Ok(Command::Help);
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "fact") {
+        let atom = parse_atom(trim_suffix(rest, '.')?)?;
+        if !atom.is_ground() {
+            return Err("facts must be ground atoms".to_string());
+        }
+        return Ok(Command::Fact(atom));
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "rule") {
+        let rule_text = trim_suffix(rest, '.')?;
+        let arrow = find_top_level_arrow(rule_text)
+            .ok_or_else(|| "rule must contain a top-level `->`".to_string())?;
+        let body_text = rule_text[..arrow].trim();
+        let head_text = rule_text[arrow + 2..].trim();
+        if body_text.is_empty() || head_text.is_empty() {
+            return Err("rule body and head must both be non-empty".to_string());
+        }
+
+        let body = parse_atom_list(body_text)?;
+        let head = parse_atom_list(head_text)?;
+        let mut builder = RuleBuilder::new();
+        for atom in body {
+            builder = builder.when(&atom.predicate, atom.terms);
+        }
+        for atom in head {
+            builder = builder.then(&atom.predicate, atom.terms);
+        }
+        return Ok(Command::Rule(builder.build()));
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "query") {
+        let atoms = parse_atom_list(trim_suffix(rest, '?')?)?;
+        return Ok(Command::Query(atoms));
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "explain") {
+        let atoms = parse_atom_list(trim_suffix(rest, '?')?)?;
+        return Ok(Command::Explain(atoms));
+    }
+
+    Err("unknown command; try `help`".to_string())
+}
+
+fn strip_keyword<'a>(input: &'a str, keyword: &str) -> Option<&'a str> {
+    let prefix = input.get(..keyword.len())?;
+    if !prefix.eq_ignore_ascii_case(keyword) {
+        return None;
+    }
+
+    let rest = input.get(keyword.len()..)?;
+    if rest.is_empty() {
+        return Some(rest);
+    }
+
+    let mut chars = rest.chars();
+    let first = chars.next()?;
+    if first.is_whitespace() {
+        Some(rest.trim_start())
+    } else {
+        None
+    }
+}
+
+fn trim_suffix(input: &str, suffix: char) -> Result<&str, String> {
+    let trimmed = input.trim();
+    if let Some(stripped) = trimmed.strip_suffix(suffix) {
+        Ok(stripped.trim_end())
+    } else {
+        Err(format!("command must end with `{}`", suffix))
+    }
+}
+
+fn parse_atom_list(input: &str) -> Result<Vec<Atom>, String> {
+    split_top_level(input, ',')?
+        .into_iter()
+        .map(parse_atom)
+        .collect()
+}
+
+fn parse_atom(input: &str) -> Result<Atom, String> {
+    let trimmed = input.trim();
+    let open = trimmed
+        .find('(')
+        .ok_or_else(|| format!("expected `(` in atom `{}`", trimmed))?;
+    let close = trimmed
+        .rfind(')')
+        .ok_or_else(|| format!("expected `)` in atom `{}`", trimmed))?;
+    if close <= open {
+        return Err(format!("malformed atom `{}`", trimmed));
+    }
+    if close != trimmed.len() - 1 {
+        return Err(format!("unexpected content after atom `{}`", trimmed));
+    }
+
+    let predicate = trimmed[..open].trim();
+    validate_identifier(predicate, "predicate")?;
+
+    let args = trimmed[open + 1..close].trim();
+    let terms = if args.is_empty() {
+        Vec::new()
+    } else {
+        split_top_level(args, ',')?
+            .into_iter()
+            .map(parse_term)
+            .collect::<Result<Vec<_>, _>>()?
+    };
+
+    Ok(Atom::new(predicate, terms))
+}
+
+fn parse_term(input: &str) -> Result<Term, String> {
+    let trimmed = input.trim();
+    if trimmed.is_empty() {
+        return Err("empty term".to_string());
+    }
+
+    if let Some(var) = trimmed.strip_prefix('?') {
+        validate_identifier(var, "variable")?;
+        return Ok(Term::var(var));
+    }
+
+    if trimmed.starts_with('"') {
+        return parse_string_literal(trimmed).map(Term::constant);
+    }
+
+    if trimmed.chars().any(char::is_whitespace) {
+        return Err(format!(
+            "constants with spaces must be quoted: `{}`",
+            trimmed
+        ));
+    }
+
+    validate_identifier(trimmed, "constant")?;
+    Ok(Term::constant(trimmed))
+}
+
+fn parse_string_literal(input: &str) -> Result<String, String> {
+    if !input.ends_with('"') || input.len() < 2 {
+        return Err(format!("unterminated string literal `{}`", input));
+    }
+
+    let inner = &input[1..input.len() - 1];
+    let mut value = String::new();
+    let mut escaped = false;
+
+    for ch in inner.chars() {
+        if escaped {
+            let translated = match ch {
+                '\\' => '\\',
+                '"' => '"',
+                'n' => '\n',
+                't' => '\t',
+                other => {
+                    return Err(format!("unsupported escape sequence `\\{}`", other));
+                }
+            };
+            value.push(translated);
+            escaped = false;
+            continue;
+        }
+
+        if ch == '\\' {
+            escaped = true;
+        } else {
+            value.push(ch);
+        }
+    }
+
+    if escaped {
+        return Err("string literal ends with a trailing escape".to_string());
+    }
+
+    Ok(value)
+}
+
+fn validate_identifier(value: &str, label: &str) -> Result<(), String> {
+    if value.is_empty() {
+        return Err(format!("{} cannot be empty", label));
+    }
+
+    if value.chars().all(is_identifier_char) {
+        Ok(())
+    } else {
+        Err(format!("invalid {} `{}`", label, value))
+    }
+}
+
+fn is_identifier_char(ch: char) -> bool {
+    ch.is_ascii_alphanumeric() || matches!(ch, '_' | '-' | ':')
+}
+
+fn find_top_level_arrow(input: &str) -> Option<usize> {
+    let bytes = input.as_bytes();
+    let mut depth = 0usize;
+    let mut in_string = false;
+    let mut escaped = false;
+    let mut index = 0usize;
+
+    while index < bytes.len() {
+        let ch = bytes[index] as char;
+        if in_string {
+            if escaped {
+                escaped = false;
+            } else if ch == '\\' {
+                escaped = true;
+            } else if ch == '"' {
+                in_string = false;
+            }
+            index += 1;
+            continue;
+        }
+
+        match ch {
+            '"' => in_string = true,
+            '(' => depth += 1,
+            ')' => depth = depth.saturating_sub(1),
+            '-' if depth == 0 && bytes.get(index + 1).copied() == Some(b'>') => {
+                return Some(index);
+            }
+            _ => {}
+        }
+        index += 1;
+    }
+
+    None
+}
+
+fn split_top_level(input: &str, separator: char) -> Result<Vec<&str>, String> {
+    let mut parts = Vec::new();
+    let mut depth = 0usize;
+    let mut in_string = false;
+    let mut escaped = false;
+    let mut start = 0usize;
+
+    for (index, ch) in input.char_indices() {
+        if in_string {
+            if escaped {
+                escaped = false;
+            } else if ch == '\\' {
+                escaped = true;
+            } else if ch == '"' {
+                in_string = false;
+            }
+            continue;
+        }
+
+        match ch {
+            '"' => in_string = true,
+            '(' => depth += 1,
+            ')' => {
+                if depth == 0 {
+                    return Err(format!("unexpected `)` in `{}`", input));
+                }
+                depth -= 1;
+            }
+            ch if ch == separator && depth == 0 => {
+                let part = input[start..index].trim();
+                if part.is_empty() {
+                    return Err(format!("empty element in `{}`", input));
+                }
+                parts.push(part);
+                start = index + ch.len_utf8();
+            }
+            _ => {}
+        }
+    }
+
+    if in_string {
+        return Err(format!("unterminated string literal in `{}`", input));
+    }
+    if depth != 0 {
+        return Err(format!("unbalanced parentheses in `{}`", input));
+    }
+
+    let tail = input[start..].trim();
+    if tail.is_empty() {
+        return Err(format!("empty element in `{}`", input));
+    }
+    parts.push(tail);
+    Ok(parts)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn parse_fact_command() {
+        let command = parse_command(r#"fact Parent(alice, "bob smith")."#).unwrap();
+        match command {
+            Command::Fact(atom) => {
+                assert_eq!(atom.predicate, "Parent");
+                assert_eq!(atom.terms.len(), 2);
+            }
+            other => panic!("unexpected command: {:?}", other),
+        }
+    }
+
+    #[test]
+    fn parse_fact_command_rejects_variables() {
+        let error = parse_command("fact Parent(?X, bob).").unwrap_err();
+        assert_eq!(error, "facts must be ground atoms");
+    }
+
+    #[test]
+    fn parse_rule_command() {
+        let command = parse_command("rule P(?X), Q(?X, a) -> R(?X).").unwrap();
+        match command {
+            Command::Rule(rule) => {
+                assert_eq!(rule.body.len(), 2);
+                assert_eq!(rule.head.len(), 1);
+            }
+            other => panic!("unexpected command: {:?}", other),
+        }
+    }
+
+    #[test]
+    fn parse_query_command() {
+        let command = parse_command("query Ancestor(?X, ?Y), Parent(?Y, ?Z)?").unwrap();
+        match command {
+            Command::Query(atoms) => assert_eq!(atoms.len(), 2),
+            other => panic!("unexpected command: {:?}", other),
+        }
+    }
+
+    #[test]
+    fn parse_explain_command() {
+        let command = parse_command("explain Ancestor(alice, carol)?").unwrap();
+        match command {
+            Command::Explain(atoms) => assert_eq!(atoms.len(), 1),
+            other => panic!("unexpected command: {:?}", other),
+        }
+    }
+
+    #[test]
+    fn parse_script_reports_line_numbers() {
+        let error = parse_script("help\nbogus\nrun.").unwrap_err();
+        assert!(error.contains("line 2"));
+    }
+}

src/frontend/mod.rs

@@ -0,0 +1,11 @@
+//! Frontend utilities for interacting with the query-engine playground.
+
+pub mod language;
+pub mod provenance;
+pub mod repl;
+pub mod session;
+pub mod web;
+
+pub use repl::run_repl;
+pub use session::Session;
+pub use web::serve_gui;

src/frontend/provenance.rs

@@ -0,0 +1,50 @@
+//! Frontend-facing provenance formatting utilities.
+
+use std::collections::HashSet;
+
+use crate::Atom;
+use crate::chase::{Derivation, MaterializedState};
+
+pub fn explain_atom(atom: &Atom, provenance: &MaterializedState) -> String {
+    let mut lines = vec![atom.to_string()];
+    let mut seen = HashSet::new();
+    render_derivation(atom, provenance, 1, &mut seen, &mut lines);
+    lines.join("\n")
+}
+
+fn render_derivation(
+    atom: &Atom,
+    state: &MaterializedState,
+    depth: usize,
+    seen: &mut HashSet<Atom>,
+    lines: &mut Vec<String>,
+) {
+    let indent = "  ".repeat(depth);
+    if !seen.insert(atom.clone()) {
+        lines.push(format!("{}already shown", indent));
+        return;
+    }
+
+    match state.provenance_for(atom) {
+        Some(Derivation::Input) => {
+            lines.push(format!("{}input fact", indent));
+        }
+        Some(Derivation::Derived {
+            rule_index,
+            rule,
+            premises,
+        }) => {
+            lines.push(format!(
+                "{}derived by rule #{}: {}",
+                indent, rule_index, rule
+            ));
+            for premise in premises {
+                lines.push(format!("{}premise: {}", indent, premise));
+                render_derivation(premise, state, depth + 1, seen, lines);
+            }
+        }
+        None => {
+            lines.push(format!("{}no provenance recorded", indent));
+        }
+    }
+}

src/frontend/repl.rs

@@ -0,0 +1,39 @@
+//! Interactive REPL for the minimal query-engine frontend language.
+
+use std::io::{self, BufRead, Write};
+
+use super::Session;
+
+pub fn run_repl() -> io::Result<()> {
+    let stdin = io::stdin();
+    let mut stdout = io::stdout();
+    let mut session = Session::new();
+
+    writeln!(stdout, "query-engine REPL")?;
+    writeln!(stdout, "Type `help` for commands and `quit` to exit.")?;
+
+    let mut lines = stdin.lock().lines();
+    loop {
+        write!(stdout, "chase> ")?;
+        stdout.flush()?;
+
+        let Some(line) = lines.next() else {
+            writeln!(stdout)?;
+            return Ok(());
+        };
+        let line = line?;
+        let trimmed = line.trim();
+        if trimmed.eq_ignore_ascii_case("quit") || trimmed.eq_ignore_ascii_case("exit") {
+            writeln!(stdout, "bye")?;
+            return Ok(());
+        }
+        if trimmed.is_empty() {
+            continue;
+        }
+
+        match session.execute_script(trimmed) {
+            Ok(output) => writeln!(stdout, "{}", output)?,
+            Err(err) => writeln!(stdout, "error: {}", err)?,
+        }
+    }
+}

src/frontend/session.rs

@@ -0,0 +1,289 @@
+//! Session state and command execution shared by the REPL and GUI.
+
+use std::fmt;
+
+use crate::chase::{
+    Atom, Instance, MaterializedState, Rule, Substitution, find_matches, materialize,
+};
+
+use super::language::{Command, parse_script};
+use super::provenance::explain_atom;
+
+#[derive(Debug, Default)]
+pub struct Session {
+    base_instance: Instance,
+    rules: Vec<Rule>,
+    materialized: Option<MaterializedState>,
+}
+
+impl Session {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn execute_script(&mut self, script: &str) -> Result<String, String> {
+        let commands = parse_script(script)?;
+        let mut output = Vec::new();
+
+        for command in commands {
+            let message = self.execute(command)?;
+            if !message.is_empty() {
+                output.push(message);
+            }
+        }
+
+        if output.is_empty() {
+            Ok("No commands executed.".to_string())
+        } else {
+            Ok(output.join("\n"))
+        }
+    }
+
+    pub fn execute(&mut self, command: Command) -> Result<String, String> {
+        match command {
+            Command::Fact(atom) => {
+                self.materialized = None;
+                let inserted = self
+                    .base_instance
+                    .try_add(atom.clone())
+                    .map_err(|err| err.to_string())?;
+                let action = if inserted {
+                    "Added"
+                } else {
+                    "Skipped duplicate"
+                };
+                Ok(format!("{} fact: {}", action, atom))
+            }
+            Command::Rule(rule) => {
+                self.materialized = None;
+                self.rules.push(rule.clone());
+                Ok(format!("Added rule #{}: {}", self.rules.len(), rule))
+            }
+            Command::Run => Ok(self.run_chase()),
+            Command::Query(query) => Ok(self.run_query(&query)),
+            Command::Explain(query) => Ok(self.explain_query(&query)),
+            Command::ShowFacts => Ok(self.show_facts()),
+            Command::ShowRules => Ok(self.show_rules()),
+            Command::Reset => {
+                *self = Self::default();
+                Ok("Session reset.".to_string())
+            }
+            Command::Help => Ok(help_text().to_string()),
+        }
+    }
+
+    pub fn reset(&mut self) {
+        *self = Self::default();
+    }
+
+    fn run_chase(&mut self) -> String {
+        let state = materialize(self.base_instance.clone(), &self.rules);
+        let message = if state.result.terminated {
+            format!(
+                "Chase completed in {} step(s); {} fact(s) available.",
+                state.result.steps,
+                state.result.instance.len()
+            )
+        } else {
+            format!(
+                "Chase stopped after {} step(s); result may be incomplete.",
+                state.result.steps
+            )
+        };
+        self.materialized = Some(state);
+        message
+    }
+
+    fn run_query(&self, query: &[Atom]) -> String {
+        let instance = self.active_instance();
+        let matches = find_matches(instance, query);
+        let variables = query_variables(query);
+
+        if variables.is_empty() {
+            return if matches.is_empty() {
+                "false".to_string()
+            } else {
+                "true".to_string()
+            };
+        }
+
+        if matches.is_empty() {
+            return "0 rows".to_string();
+        }
+
+        let mut rows = matches
+            .iter()
+            .map(|subst| format_substitution(subst, &variables))
+            .collect::<Vec<_>>();
+        rows.sort();
+
+        let mut rendered = Vec::with_capacity(rows.len() + 1);
+        rendered.push(format!("{} row(s)", rows.len()));
+        rendered.extend(rows);
+        rendered.join("\n")
+    }
+
+    fn explain_query(&self, query: &[Atom]) -> String {
+        let instance = self.active_instance();
+        let matches = find_matches(instance, query);
+        if matches.is_empty() {
+            return if self.materialized.is_none() && !self.rules.is_empty() {
+                "0 explanations. Run `run.` first to trace derived answers.".to_string()
+            } else {
+                "0 explanations".to_string()
+            };
+        }
+
+        let variables = query_variables(query);
+        let mut sections = Vec::new();
+
+        for (index, subst) in matches.iter().enumerate() {
+            let mut lines = Vec::new();
+            lines.push(format!("match {}", index + 1));
+            if !variables.is_empty() {
+                lines.push(format!("  {}", format_substitution(subst, &variables)));
+            }
+
+            for atom in query.iter().map(|atom| subst.apply_atom(atom)) {
+                lines.push(format!("  answer atom: {}", atom));
+                if let Some(state) = &self.materialized {
+                    for detail in explain_atom(&atom, state).lines().skip(1) {
+                        lines.push(format!("  {}", detail));
+                    }
+                } else {
+                    lines.push("    input fact".to_string());
+                }
+            }
+
+            sections.push(lines.join("\n"));
+        }
+
+        let mut output = vec![format!("{} explanation(s)", sections.len())];
+        output.extend(sections);
+        output.join("\n")
+    }
+
+    fn show_facts(&self) -> String {
+        let facts = sorted_render(self.active_instance().iter());
+        if facts.is_empty() {
+            return "No facts loaded.".to_string();
+        }
+
+        facts.join("\n")
+    }
+
+    fn show_rules(&self) -> String {
+        if self.rules.is_empty() {
+            return "No rules loaded.".to_string();
+        }
+
+        self.rules
+            .iter()
+            .enumerate()
+            .map(|(index, rule)| format!("{}: {}", index + 1, rule))
+            .collect::<Vec<_>>()
+            .join("\n")
+    }
+
+    fn active_instance(&self) -> &Instance {
+        if let Some(result) = &self.materialized {
+            &result.result.instance
+        } else {
+            &self.base_instance
+        }
+    }
+}
+
+fn help_text() -> &'static str {
+    "Commands:
+fact Parent(alice, bob).
+rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
+run.
+query Ancestor(?X, ?Y)?
+explain Ancestor(alice, bob)?
+show facts
+show rules
+reset
+help"
+}
+
+fn sorted_render<'a, T>(items: impl Iterator<Item = &'a T>) -> Vec<String>
+where
+    T: fmt::Display + 'a,
+{
+    let mut rendered = items.map(ToString::to_string).collect::<Vec<_>>();
+    rendered.sort();
+    rendered
+}
+
+fn query_variables(query: &[Atom]) -> Vec<String> {
+    let mut variables = query
+        .iter()
+        .flat_map(|atom| atom.variables())
+        .cloned()
+        .collect::<Vec<_>>();
+    variables.sort();
+    variables.dedup();
+    variables
+}
+
+fn format_substitution(subst: &Substitution, variables: &[String]) -> String {
+    variables
+        .iter()
+        .filter_map(|var| subst.get(var).map(|term| format!("?{} = {}", var, term)))
+        .collect::<Vec<_>>()
+        .join(", ")
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn session_runs_chase_and_query() {
+        let mut session = Session::new();
+        let output = session
+            .execute_script(
+                "fact Parent(alice, bob).\n\
+                 fact Parent(bob, carol).\n\
+                 rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).\n\
+                 rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z).\n\
+                 run.\n\
+                 query Ancestor(?X, ?Y)?",
+            )
+            .unwrap();
+
+        assert!(output.contains("Chase completed"));
+        assert!(output.contains("?X = alice, ?Y = bob"));
+        assert!(output.contains("?X = alice, ?Y = carol"));
+    }
+
+    #[test]
+    fn boolean_query_returns_truth_value() {
+        let mut session = Session::new();
+        let output = session
+            .execute_script("fact Parent(alice, bob).\nquery Parent(alice, bob)?")
+            .unwrap();
+        assert!(output.ends_with("true"));
+    }
+
+    #[test]
+    fn explain_query_shows_rule_trace() {
+        let mut session = Session::new();
+        let output = session
+            .execute_script(
+                "fact Parent(alice, bob).\n\
+                 fact Parent(bob, carol).\n\
+                 rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).\n\
+                 rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z).\n\
+                 run.\n\
+                 explain Ancestor(alice, carol)?",
+            )
+            .unwrap();
+
+        assert!(output.contains("explanation(s)"));
+        assert!(output.contains("derived by rule #2"));
+        assert!(output.contains("premise: Ancestor(alice, bob)"));
+        assert!(output.contains("input fact"));
+    }
+}

src/frontend/web.rs

@@ -0,0 +1,286 @@
+//! Minimal local web UI for the query-engine frontend language.
+
+use std::io::{self, BufRead, BufReader, Read, Write};
+use std::net::{TcpListener, TcpStream};
+use std::sync::{Arc, Mutex};
+
+use super::Session;
+
+pub fn serve_gui(address: &str) -> io::Result<()> {
+    let listener = TcpListener::bind(address)?;
+    let session = Arc::new(Mutex::new(Session::new()));
+
+    println!("GUI available at http://{}", address);
+
+    for stream in listener.incoming() {
+        match stream {
+            Ok(stream) => {
+                let shared = Arc::clone(&session);
+                if let Err(err) = handle_connection(stream, &shared) {
+                    eprintln!("gui error: {}", err);
+                }
+            }
+            Err(err) => eprintln!("gui accept error: {}", err),
+        }
+    }
+
+    Ok(())
+}
+
+fn handle_connection(mut stream: TcpStream, session: &Arc<Mutex<Session>>) -> io::Result<()> {
+    let mut reader = BufReader::new(stream.try_clone()?);
+    let mut request_line = String::new();
+    reader.read_line(&mut request_line)?;
+    if request_line.trim().is_empty() {
+        return Ok(());
+    }
+
+    let mut parts = request_line.split_whitespace();
+    let method = parts.next().unwrap_or_default();
+    let path = parts.next().unwrap_or("/");
+
+    let mut content_length = 0usize;
+    loop {
+        let mut header = String::new();
+        reader.read_line(&mut header)?;
+        if header == "\r\n" || header.is_empty() {
+            break;
+        }
+        if let Some((name, value)) = header.split_once(':')
+            && name.eq_ignore_ascii_case("content-length")
+        {
+            let parsed = value.trim().parse::<usize>().ok();
+            if let Some(length) = parsed {
+                content_length = length;
+            }
+        }
+    }
+
+    let mut body = vec![0u8; content_length];
+    if content_length > 0 {
+        reader.read_exact(&mut body)?;
+    }
+
+    let response = match (method, path) {
+        ("GET", "/") => http_response("200 OK", "text/html; charset=utf-8", INDEX_HTML),
+        ("POST", "/execute") => {
+            let script = String::from_utf8_lossy(&body);
+            let output = {
+                let mut locked = session
+                    .lock()
+                    .map_err(|_| io::Error::other("session lock poisoned"))?;
+                match locked.execute_script(script.as_ref()) {
+                    Ok(output) => output,
+                    Err(err) => format!("error: {}", err),
+                }
+            };
+            http_response("200 OK", "text/plain; charset=utf-8", &output)
+        }
+        ("POST", "/reset") => {
+            let mut locked = session
+                .lock()
+                .map_err(|_| io::Error::other("session lock poisoned"))?;
+            locked.reset();
+            http_response("200 OK", "text/plain; charset=utf-8", "Session reset.")
+        }
+        _ => http_response("404 Not Found", "text/plain; charset=utf-8", "Not found"),
+    };
+
+    stream.write_all(response.as_bytes())?;
+    stream.flush()?;
+    Ok(())
+}
+
+fn http_response(status: &str, content_type: &str, body: &str) -> String {
+    format!(
+        "HTTP/1.1 {}\r\nContent-Type: {}\r\nContent-Length: {}\r\nConnection: close\r\n\r\n{}",
+        status,
+        content_type,
+        body.len(),
+        body
+    )
+}
+
+const INDEX_HTML: &str = r#"<!DOCTYPE html>
+<html lang="en">
+<head>
+  <meta charset="utf-8">
+  <meta name="viewport" content="width=device-width, initial-scale=1">
+  <title>query-engine GUI</title>
+  <style>
+    :root {
+      --bg: #f4efe6;
+      --panel: rgba(255, 251, 245, 0.9);
+      --ink: #1f1d1a;
+      --accent: #b5542f;
+      --accent-soft: #e7c7b8;
+      --border: #d7c7b8;
+      --shadow: rgba(78, 52, 38, 0.14);
+    }
+
+    * { box-sizing: border-box; }
+
+    body {
+      margin: 0;
+      min-height: 100vh;
+      font-family: "Iosevka", "SFMono-Regular", "Menlo", monospace;
+      color: var(--ink);
+      background:
+        radial-gradient(circle at top left, rgba(181, 84, 47, 0.18), transparent 28rem),
+        linear-gradient(135deg, #efe4d4, var(--bg));
+    }
+
+    main {
+      width: min(1100px, calc(100% - 2rem));
+      margin: 2rem auto;
+      display: grid;
+      gap: 1rem;
+      grid-template-columns: repeat(auto-fit, minmax(320px, 1fr));
+    }
+
+    section {
+      background: var(--panel);
+      border: 1px solid var(--border);
+      border-radius: 18px;
+      box-shadow: 0 18px 50px var(--shadow);
+      backdrop-filter: blur(10px);
+    }
+
+    .editor {
+      padding: 1.25rem;
+    }
+
+    .header {
+      display: flex;
+      justify-content: space-between;
+      align-items: center;
+      gap: 1rem;
+      margin-bottom: 1rem;
+    }
+
+    h1, h2, p {
+      margin: 0;
+    }
+
+    h1 {
+      font-size: clamp(1.5rem, 2vw, 2rem);
+      letter-spacing: 0.04em;
+      text-transform: uppercase;
+    }
+
+    p {
+      color: rgba(31, 29, 26, 0.74);
+      line-height: 1.5;
+    }
+
+    textarea {
+      width: 100%;
+      min-height: 22rem;
+      border: 1px solid var(--border);
+      border-radius: 14px;
+      background: #fffdfa;
+      color: var(--ink);
+      padding: 1rem;
+      resize: vertical;
+      font: inherit;
+      line-height: 1.5;
+    }
+
+    .actions {
+      display: flex;
+      gap: 0.75rem;
+      margin-top: 1rem;
+      flex-wrap: wrap;
+    }
+
+    button {
+      border: 0;
+      border-radius: 999px;
+      padding: 0.8rem 1.2rem;
+      font: inherit;
+      cursor: pointer;
+      transition: transform 140ms ease, opacity 140ms ease;
+    }
+
+    button:hover { transform: translateY(-1px); }
+    button:active { transform: translateY(0); }
+
+    .primary {
+      background: var(--accent);
+      color: #fff8f3;
+    }
+
+    .secondary {
+      background: var(--accent-soft);
+      color: var(--ink);
+    }
+
+    pre {
+      margin: 0;
+      padding: 1.25rem;
+      min-height: 100%;
+      white-space: pre-wrap;
+      word-break: break-word;
+      line-height: 1.5;
+    }
+
+    .output {
+      overflow: hidden;
+    }
+
+    .sample {
+      font-size: 0.92rem;
+      padding: 0 1.25rem 1.25rem;
+    }
+  </style>
+</head>
+<body>
+  <main>
+    <section class="editor">
+      <div class="header">
+        <div>
+          <h1>query-engine</h1>
+          <p>Minimal local workbench for rule-driven query experiments.</p>
+        </div>
+      </div>
+      <textarea id="script">fact Parent(alice, bob).
+fact Parent(bob, carol).
+rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
+rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z).
+run.
+explain Ancestor(alice, carol)?</textarea>
+      <div class="actions">
+        <button class="primary" id="execute">Execute</button>
+        <button class="secondary" id="reset">Reset Session</button>
+      </div>
+      <p class="sample">Try <code>query Ancestor(?X, ?Y)?</code>, <code>explain Ancestor(alice, carol)?</code>, or boolean queries like <code>query Parent(alice, bob)?</code>.</p>
+    </section>
+
+    <section class="output">
+      <pre id="output">Session ready.</pre>
+    </section>
+  </main>
+
+  <script>
+    const output = document.getElementById("output");
+    const script = document.getElementById("script");
+
+    async function send(path, body) {
+      const response = await fetch(path, { method: "POST", body });
+      const text = await response.text();
+      return text;
+    }
+
+    document.getElementById("execute").addEventListener("click", async () => {
+      const text = await send("/execute", script.value);
+      output.textContent += `\n\n> ${new Date().toLocaleTimeString()}\n${text}`;
+    });
+
+    document.getElementById("reset").addEventListener("click", async () => {
+      const text = await send("/reset", "");
+      output.textContent = text;
+    });
+  </script>
+</body>
+</html>
+"#;

src/lib.rs

@@ -0,0 +1,15 @@
+//! Query-engine playground crate.
+//!
+//! The current codebase primarily contains a chase-based reasoning core plus
+//! 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 chase;
+pub mod frontend;
+
+// Curated convenience re-exports for the current public crate surface.
+// Lower-level reasoning and provenance APIs remain under `query_engine::chase`.
+pub use chase::{
+    Atom, ChaseConfig, ChaseError, ChaseResult, ChaseVariant, Instance, Rule, RuleBuilder, Term,
+    chase, chase_with_config, standard_chase,
+};

src/main.rs

@@ -0,0 +1,42 @@
+use std::env;
+use std::fs;
+use std::io;
+
+use query_engine::frontend::{Session, run_repl, serve_gui};
+
+fn main() -> io::Result<()> {
+    let args = env::args().skip(1).collect::<Vec<_>>();
+    if args.is_empty() {
+        return run_repl();
+    }
+
+    match args.as_slice() {
+        [cmd] if cmd.eq_ignore_ascii_case("repl") => run_repl(),
+        [cmd] if cmd.eq_ignore_ascii_case("gui") => serve_gui("127.0.0.1:7878"),
+        [cmd, address] if cmd.eq_ignore_ascii_case("gui") => serve_gui(address),
+        [cmd, path] if cmd.eq_ignore_ascii_case("script") => run_script(path),
+        _ => {
+            print_usage();
+            Ok(())
+        }
+    }
+}
+
+fn run_script(path: &str) -> io::Result<()> {
+    let script = fs::read_to_string(path)?;
+    let mut session = Session::new();
+    match session.execute_script(&script) {
+        Ok(output) => {
+            println!("{}", output);
+            Ok(())
+        }
+        Err(err) => Err(io::Error::new(io::ErrorKind::InvalidInput, err)),
+    }
+}
+
+fn print_usage() {
+    println!("Usage:");
+    println!("  query-engine repl");
+    println!("  query-engine gui [host:port]");
+    println!("  query-engine script <path>");
+}

tests/integration_tests.rs

@@ -0,0 +1,187 @@
+//! Integration tests for the current rule-engine core.
+
+use query_engine::chase::rule::RuleBuilder;
+use query_engine::{Atom, Instance, Term, chase};
+
+#[test]
+fn test_transitive_closure() {
+    // Build a chain: a -> b -> c -> d
+    let instance: Instance = vec![
+        Atom::new("Edge", vec![Term::constant("a"), Term::constant("b")]),
+        Atom::new("Edge", vec![Term::constant("b"), Term::constant("c")]),
+        Atom::new("Edge", vec![Term::constant("c"), Term::constant("d")]),
+    ]
+    .into_iter()
+    .collect();
+
+    // Edge(X, Y) -> Path(X, Y)
+    let rule1 = RuleBuilder::new()
+        .when("Edge", vec![Term::var("X"), Term::var("Y")])
+        .then("Path", vec![Term::var("X"), Term::var("Y")])
+        .build();
+
+    // Path(X, Y), Edge(Y, Z) -> Path(X, Z)
+    let rule2 = RuleBuilder::new()
+        .when("Path", vec![Term::var("X"), Term::var("Y")])
+        .when("Edge", vec![Term::var("Y"), Term::var("Z")])
+        .then("Path", vec![Term::var("X"), Term::var("Z")])
+        .build();
+
+    let result = chase(instance, &[rule1, rule2]);
+
+    assert!(result.terminated);
+
+    // Should have 6 paths: a->b, b->c, c->d, a->c, b->d, a->d
+    let paths = result.instance.facts_for_predicate("Path");
+    assert_eq!(paths.len(), 6);
+}
+
+#[test]
+fn test_existential_rule_generates_nulls() {
+    // Every employee must have a department
+    let instance: Instance = vec![
+        Atom::new("Employee", vec![Term::constant("alice")]),
+        Atom::new("Employee", vec![Term::constant("bob")]),
+        Atom::new("Employee", vec![Term::constant("carol")]),
+    ]
+    .into_iter()
+    .collect();
+
+    // Employee(X) -> WorksIn(X, Y) where Y is existential
+    let rule = RuleBuilder::new()
+        .when("Employee", vec![Term::var("X")])
+        .then("WorksIn", vec![Term::var("X"), Term::var("Dept")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+
+    let works_in = result.instance.facts_for_predicate("WorksIn");
+    assert_eq!(works_in.len(), 3);
+
+    // Each should have a unique null
+    let nulls: Vec<_> = works_in
+        .iter()
+        .filter_map(|f| match &f.terms[1] {
+            Term::Null(id) => Some(*id),
+            _ => None,
+        })
+        .collect();
+    assert_eq!(nulls.len(), 3);
+
+    // All nulls should be unique
+    let mut unique_nulls = nulls.clone();
+    unique_nulls.sort();
+    unique_nulls.dedup();
+    assert_eq!(unique_nulls.len(), 3);
+}
+
+#[test]
+fn test_multiple_head_atoms() {
+    let instance: Instance = vec![Atom::new("Person", vec![Term::constant("alice")])]
+        .into_iter()
+        .collect();
+
+    // Person(X) -> HasName(X, N), HasAge(X, A)
+    let rule = RuleBuilder::new()
+        .when("Person", vec![Term::var("X")])
+        .then("HasName", vec![Term::var("X"), Term::var("N")])
+        .then("HasAge", vec![Term::var("X"), Term::var("A")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+    assert_eq!(result.instance.facts_for_predicate("HasName").len(), 1);
+    assert_eq!(result.instance.facts_for_predicate("HasAge").len(), 1);
+}
+
+#[test]
+fn test_chase_with_constants_in_rules() {
+    let instance: Instance = vec![
+        Atom::new(
+            "Status",
+            vec![Term::constant("alice"), Term::constant("active")],
+        ),
+        Atom::new(
+            "Status",
+            vec![Term::constant("bob"), Term::constant("inactive")],
+        ),
+    ]
+    .into_iter()
+    .collect();
+
+    // Only active users get access: Status(X, "active") -> HasAccess(X)
+    let rule = RuleBuilder::new()
+        .when("Status", vec![Term::var("X"), Term::constant("active")])
+        .then("HasAccess", vec![Term::var("X")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+
+    let access = result.instance.facts_for_predicate("HasAccess");
+    assert_eq!(access.len(), 1);
+
+    // Only alice should have access
+    let fact = access[0];
+    assert_eq!(fact.terms[0], Term::constant("alice"));
+}
+
+#[test]
+fn test_chase_reaches_fixpoint() {
+    // Test that applying the same rule multiple times doesn't create duplicates
+    let instance: Instance = vec![Atom::new("Fact", vec![Term::constant("x")])]
+        .into_iter()
+        .collect();
+
+    // Fact(X) -> Derived(X)
+    let rule = RuleBuilder::new()
+        .when("Fact", vec![Term::var("X")])
+        .then("Derived", vec![Term::var("X")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+    assert_eq!(result.instance.facts_for_predicate("Derived").len(), 1);
+    assert_eq!(result.steps, 1); // Should complete in one step
+}
+
+#[test]
+fn test_self_join_rule() {
+    // Find pairs of people with the same manager
+    let instance: Instance = vec![
+        Atom::new(
+            "ManagedBy",
+            vec![Term::constant("alice"), Term::constant("eve")],
+        ),
+        Atom::new(
+            "ManagedBy",
+            vec![Term::constant("bob"), Term::constant("eve")],
+        ),
+        Atom::new(
+            "ManagedBy",
+            vec![Term::constant("carol"), Term::constant("frank")],
+        ),
+    ]
+    .into_iter()
+    .collect();
+
+    // ManagedBy(X, M), ManagedBy(Y, M) -> SameTeam(X, Y)
+    let rule = RuleBuilder::new()
+        .when("ManagedBy", vec![Term::var("X"), Term::var("M")])
+        .when("ManagedBy", vec![Term::var("Y"), Term::var("M")])
+        .then("SameTeam", vec![Term::var("X"), Term::var("Y")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+
+    // Should have: (alice, alice), (alice, bob), (bob, alice), (bob, bob), (carol, carol)
+    let same_team = result.instance.facts_for_predicate("SameTeam");
+    assert_eq!(same_team.len(), 5);
+}

tests/property_tests.rs

@@ -0,0 +1,444 @@
+//! Property-based tests for the current rule-engine core using proptest.
+//!
+//! All tests use explicit seeds for reproducibility.
+
+use proptest::prelude::*;
+use proptest::test_runner::{Config, TestRng, TestRunner};
+
+use query_engine::chase::Substitution;
+use query_engine::chase::rule::RuleBuilder;
+use query_engine::{Atom, Instance, Term, chase};
+
+// =============================================================================
+// Test Configuration
+// =============================================================================
+
+/// Create a test runner with an explicit seed for reproducibility.
+fn seeded_runner(seed: u64, cases: u32) -> TestRunner {
+    let config = Config::with_cases(cases);
+    // Create a deterministic seed from u64
+    let mut seed_bytes = [0u8; 32];
+    seed_bytes[..8].copy_from_slice(&seed.to_le_bytes());
+    let rng = TestRng::from_seed(proptest::test_runner::RngAlgorithm::ChaCha, &seed_bytes);
+    TestRunner::new_with_rng(config, rng)
+}
+
+// =============================================================================
+// Strategies
+// =============================================================================
+
+/// Strategy for generating constant names
+fn constant_strategy() -> impl Strategy<Value = String> {
+    prop::sample::select(vec![
+        "a".to_string(),
+        "b".to_string(),
+        "c".to_string(),
+        "d".to_string(),
+        "e".to_string(),
+    ])
+}
+
+/// Strategy for generating variable names
+fn variable_strategy() -> impl Strategy<Value = String> {
+    prop::sample::select(vec![
+        "X".to_string(),
+        "Y".to_string(),
+        "Z".to_string(),
+        "W".to_string(),
+    ])
+}
+
+/// Strategy for generating predicate names
+fn predicate_strategy() -> impl Strategy<Value = String> {
+    prop::sample::select(vec![
+        "P".to_string(),
+        "Q".to_string(),
+        "R".to_string(),
+        "S".to_string(),
+    ])
+}
+
+/// Strategy for generating ground atoms (facts)
+fn ground_atom_strategy() -> impl Strategy<Value = Atom> {
+    (
+        predicate_strategy(),
+        prop::collection::vec(constant_strategy(), 1..=3),
+    )
+        .prop_map(|(pred, consts)| {
+            Atom::new(pred, consts.into_iter().map(Term::constant).collect())
+        })
+}
+
+/// Strategy for generating a small instance (set of facts)
+fn instance_strategy() -> impl Strategy<Value = Instance> {
+    prop::collection::vec(ground_atom_strategy(), 0..10)
+        .prop_map(|atoms| atoms.into_iter().collect())
+}
+
+// =============================================================================
+// Property: Chase always terminates
+// =============================================================================
+
+#[test]
+fn chase_always_terminates() {
+    const SEED: u64 = 12345;
+    let mut runner = seeded_runner(SEED, 50);
+
+    runner
+        .run(&instance_strategy(), |instance| {
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
+                .build();
+
+            let result = chase(instance, &[rule]);
+
+            prop_assert!(result.terminated || result.steps > 0);
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Chase is monotonic (facts are only added, never removed)
+// =============================================================================
+
+#[test]
+fn chase_is_monotonic() {
+    const SEED: u64 = 23456;
+    let mut runner = seeded_runner(SEED, 50);
+
+    runner
+        .run(&instance_strategy(), |instance| {
+            let initial_facts: Vec<_> = instance.iter().cloned().collect();
+
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
+                .build();
+
+            let result = chase(instance, &[rule]);
+
+            for fact in &initial_facts {
+                prop_assert!(
+                    result.instance.contains(fact),
+                    "Original fact {:?} was removed",
+                    fact
+                );
+            }
+
+            prop_assert!(result.instance.len() >= initial_facts.len());
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Fixpoint is stable (running chase again produces no changes)
+// =============================================================================
+
+#[test]
+fn fixpoint_is_stable() {
+    const SEED: u64 = 34567;
+    let mut runner = seeded_runner(SEED, 30);
+
+    runner
+        .run(&instance_strategy(), |instance| {
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
+                .build();
+
+            let result1 = chase(instance, std::slice::from_ref(&rule));
+            prop_assert!(result1.terminated);
+
+            let result2 = chase(result1.instance.clone(), &[rule]);
+
+            prop_assert!(result2.terminated);
+            prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
+            prop_assert_eq!(result1.instance.len(), result2.instance.len());
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: All derived facts are ground (no variables)
+// =============================================================================
+
+#[test]
+fn all_facts_are_ground() {
+    const SEED: u64 = 45678;
+    let mut runner = seeded_runner(SEED, 50);
+
+    runner
+        .run(&instance_strategy(), |instance| {
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X"), Term::var("Y")])
+                .then("R", vec![Term::var("X"), Term::var("Y")])
+                .build();
+
+            let result = chase(instance, &[rule]);
+
+            for fact in result.instance.iter() {
+                prop_assert!(fact.is_ground(), "Fact {:?} contains variables", fact);
+            }
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Rules without existentials don't create nulls
+// =============================================================================
+
+#[test]
+fn no_existentials_means_no_nulls() {
+    const SEED: u64 = 56789;
+    let mut runner = seeded_runner(SEED, 50);
+
+    runner
+        .run(&instance_strategy(), |instance| {
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
+                .build();
+
+            let result = chase(instance, &[rule]);
+
+            for fact in result.instance.iter() {
+                for term in &fact.terms {
+                    prop_assert!(
+                        !matches!(term, Term::Null(_)),
+                        "Found null in fact {:?} but rule has no existentials",
+                        fact
+                    );
+                }
+            }
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Existential rules create exactly one null per trigger
+// =============================================================================
+
+#[test]
+fn existentials_create_unique_nulls() {
+    const SEED: u64 = 67890;
+    let mut runner = seeded_runner(SEED, 30);
+
+    runner
+        .run(&(1usize..5), |num_constants| {
+            let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
+            let instance: Instance = constants
+                .iter()
+                .map(|c| Atom::new("P", vec![Term::constant(c)]))
+                .collect();
+
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X"), Term::var("Y")])
+                .build();
+
+            let result = chase(instance, &[rule]);
+
+            let q_facts: Vec<_> = result.instance.facts_for_predicate("Q");
+
+            prop_assert_eq!(q_facts.len(), num_constants);
+
+            for fact in &q_facts {
+                prop_assert!(
+                    matches!(fact.terms[1], Term::Null(_)),
+                    "Expected null in second position of {:?}",
+                    fact
+                );
+            }
+
+            let nulls: Vec<_> = q_facts
+                .iter()
+                .filter_map(|f| match &f.terms[1] {
+                    Term::Null(id) => Some(*id),
+                    _ => None,
+                })
+                .collect();
+
+            let mut unique_nulls = nulls.clone();
+            unique_nulls.sort();
+            unique_nulls.dedup();
+            prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Transitive closure computes correct number of facts
+// =============================================================================
+
+#[test]
+fn transitive_closure_chain() {
+    const SEED: u64 = 78901;
+    let mut runner = seeded_runner(SEED, 20);
+
+    runner
+        .run(&(2usize..6), |chain_length| {
+            let mut facts = Vec::new();
+            for i in 0..chain_length {
+                facts.push(Atom::new(
+                    "E",
+                    vec![
+                        Term::constant(format!("{}", i)),
+                        Term::constant(format!("{}", i + 1)),
+                    ],
+                ));
+            }
+            let instance: Instance = facts.into_iter().collect();
+
+            let rule1 = RuleBuilder::new()
+                .when("E", vec![Term::var("X"), Term::var("Y")])
+                .then("T", vec![Term::var("X"), Term::var("Y")])
+                .build();
+
+            let rule2 = RuleBuilder::new()
+                .when("T", vec![Term::var("X"), Term::var("Y")])
+                .when("E", vec![Term::var("Y"), Term::var("Z")])
+                .then("T", vec![Term::var("X"), Term::var("Z")])
+                .build();
+
+            let result = chase(instance, &[rule1, rule2]);
+            prop_assert!(result.terminated);
+
+            let t_facts = result.instance.facts_for_predicate("T");
+
+            let expected = chain_length * (chain_length + 1) / 2;
+            prop_assert_eq!(
+                t_facts.len(),
+                expected,
+                "Chain of {} edges should have {} transitive pairs",
+                chain_length,
+                expected
+            );
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Empty instance with any rules produces empty or stays empty
+// =============================================================================
+
+#[test]
+fn empty_instance_stays_bounded() {
+    const SEED: u64 = 89012;
+    let mut runner = seeded_runner(SEED, 100);
+
+    runner
+        .run(&(0u64..1000), |_| {
+            let instance = Instance::new();
+
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
+                .build();
+
+            let result = chase(instance, &[rule]);
+
+            prop_assert!(result.terminated);
+            prop_assert_eq!(result.steps, 0);
+            prop_assert!(result.instance.is_empty());
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Substitution application is idempotent for ground terms
+// =============================================================================
+
+#[test]
+fn substitution_ground_term_unchanged() {
+    const SEED: u64 = 90123;
+    let mut runner = seeded_runner(SEED, 100);
+
+    runner
+        .run(&constant_strategy(), |c| {
+            let term = Term::constant(&c);
+            let mut subst = Substitution::new();
+            subst.bind("X".to_string(), Term::constant("other"));
+
+            let result = subst.apply_term(&term);
+
+            prop_assert_eq!(
+                result,
+                term,
+                "Ground term should be unchanged by substitution"
+            );
+            Ok(())
+        })
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Substitution correctly replaces variables
+// =============================================================================
+
+#[test]
+fn substitution_replaces_variable() {
+    const SEED: u64 = 11111;
+    let mut runner = seeded_runner(SEED, 100);
+
+    runner
+        .run(
+            &(variable_strategy(), constant_strategy()),
+            |(var, replacement)| {
+                let term = Term::var(&var);
+                let mut subst = Substitution::new();
+                subst.bind(var.clone(), Term::constant(&replacement));
+
+                let result = subst.apply_term(&term);
+
+                prop_assert_eq!(
+                    result,
+                    Term::constant(&replacement),
+                    "Variable should be replaced"
+                );
+                Ok(())
+            },
+        )
+        .unwrap();
+}
+
+// =============================================================================
+// Property: Atom arity is preserved through substitution
+// =============================================================================
+
+#[test]
+fn substitution_preserves_arity() {
+    const SEED: u64 = 22222;
+    let mut runner = seeded_runner(SEED, 50);
+
+    let strategy = (
+        predicate_strategy(),
+        prop::collection::vec(variable_strategy(), 1..4),
+        constant_strategy(),
+    );
+
+    runner
+        .run(&strategy, |(pred, vars, replacement)| {
+            let atom = Atom::new(&pred, vars.iter().map(Term::var).collect());
+
+            let mut subst = Substitution::new();
+            for var in &vars {
+                subst.bind(var.clone(), Term::constant(&replacement));
+            }
+
+            let result = subst.apply_atom(&atom);
+
+            prop_assert_eq!(result.arity(), atom.arity());
+            prop_assert_eq!(result.predicate, atom.predicate);
+            Ok(())
+        })
+        .unwrap();
+}

tests/regression_tests.rs

@@ -0,0 +1,95 @@
+use query_engine::chase::materialize;
+use query_engine::chase::rule::RuleBuilder;
+use query_engine::frontend::Session;
+use query_engine::{Atom, Instance, Term, chase};
+
+#[test]
+fn existential_trigger_stays_inactive_when_head_is_already_satisfied() {
+    let instance: Instance = vec![
+        Atom::new("Person", vec![Term::constant("alice")]),
+        Atom::new(
+            "HasSSN",
+            vec![Term::constant("alice"), Term::constant("known")],
+        ),
+    ]
+    .into_iter()
+    .collect();
+
+    let rule = RuleBuilder::new()
+        .when("Person", vec![Term::var("X")])
+        .then("HasSSN", vec![Term::var("X"), Term::var("Y")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+    assert_eq!(result.steps, 0);
+    assert_eq!(result.instance.facts_for_predicate("HasSSN").len(), 1);
+}
+
+#[test]
+fn fresh_nulls_skip_existing_input_null_ids() {
+    let instance: Instance = vec![
+        Atom::new("Seed", vec![Term::null(0)]),
+        Atom::new("Person", vec![Term::constant("alice")]),
+    ]
+    .into_iter()
+    .collect();
+
+    let rule = RuleBuilder::new()
+        .when("Person", vec![Term::var("X")])
+        .then("HasSSN", vec![Term::var("X"), Term::var("Y")])
+        .build();
+
+    let result = chase(instance, &[rule]);
+
+    assert!(result.terminated);
+    assert_eq!(result.instance.facts_for_predicate("HasSSN").len(), 1);
+
+    let fact = result.instance.facts_for_predicate("HasSSN")[0];
+    assert!(matches!(fact.terms[1], Term::Null(id) if id > 0));
+}
+
+#[test]
+fn frontend_materialization_respects_existing_existential_witnesses() {
+    let mut session = Session::new();
+    let output = session
+        .execute_script(
+            "fact Person(alice).\n\
+             fact HasSSN(alice, known).\n\
+             rule Person(?X) -> HasSSN(?X, ?Y).\n\
+             run.\n\
+             query HasSSN(alice, ?Y)?",
+        )
+        .unwrap();
+
+    assert!(output.contains("1 row(s)"));
+    assert!(output.contains("?Y = known"));
+    assert!(!output.contains("⊥"));
+}
+
+#[test]
+fn frontend_materialization_starts_after_existing_null_ids() {
+    let instance: Instance = vec![
+        Atom::new("Seed", vec![Term::null(7)]),
+        Atom::new("Employee", vec![Term::constant("alice")]),
+    ]
+    .into_iter()
+    .collect();
+
+    let rule = RuleBuilder::new()
+        .when("Employee", vec![Term::var("X")])
+        .then("WorksIn", vec![Term::var("X"), Term::var("Dept")])
+        .build();
+
+    let state = materialize(instance, &[rule]);
+
+    assert!(state.result.terminated);
+    assert_eq!(
+        state.result.instance.facts_for_predicate("WorksIn").len(),
+        1
+    );
+
+    let fact = state.result.instance.facts_for_predicate("WorksIn")[0];
+    assert!(matches!(fact.terms[1], Term::Null(id) if id > 7));
+}