## Projects Related to Geolog

### Chase-Based & Geometric Logic Tools

| Project                                                            | Language | Description                                                                                                                   | Key Features                                                                                                         | Link                                                                              |
|--------------------------------------------------------------------|----------|-------------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------|
| **Chase** (Ramsdell)                                               | OCaml    | Model finder for finitary geometric logic. Uses an input syntax called "Geolog" — likely the direct namesake of this project. | Minimal model finding, partial functions, tree visualization of chase output, Prolog-like input syntax (`.gl` files) | [github.com/ramsdell/chase](<https://github.com/ramsdell/chase>)                  |
| **Rusty Razor**                                                    | Rust     | First-order model finder using the chase algorithm. Converts arbitrary FOL to geometric normal form.                          | Homomorphically minimal models, no upfront bound required, model space exploration, provenance tracking              | [github.com/salmans/rusty-razor](<https://github.com/salmans/rusty-razor>)        |
| **Geometric Logic for Policy Analysis** (Sagha, Naumov, Dougherty) | Haskell  | Chase-based prototype for analyzing access control policies as geometric theories.                                            | Jointly universal model sets, policy verification, comparison with SAT-based tools like Kodkod/Margrave              | [Paper (PDF)](<https://cs.brown.edu/~tbn/publications/snd-arsec13-geometric.pdf>) |

### Applied Category Theory Tools

| Project                        | Language          | Description                                                                                                          | Key Features                                                                                                | Link                                                                                                                         |
|--------------------------------|-------------------|----------------------------------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------------------|------------------------------------------------------------------------------------------------------------------------------|
| **Catlab.jl**                  | Julia             | Framework for applied and computational category theory. The most mature library in this space.                      | Generalized algebraic theories (GATs), C-sets/acsets, chase algorithm, wiring diagrams, limits/colimits     | [github.com/AlgebraicJulia/Catlab.jl](<https://github.com/AlgebraicJulia/Catlab.jl>)                                         |
| **CatColab** (Topos Institute) | Rust + TypeScript | Collaborative web environment for formal, interoperable conceptual modeling. Closest in *spirit* to Geolog's vision. | Notebook UI, multiple domain-specific logics, collaborative editing, double-theory framework, visualization | [github.com/ToposInstitute/CatColab](<https://github.com/ToposInstitute/CatColab>) / [catcolab.org](<https://catcolab.org/>) |
| **AlgebraicJulia** (ecosystem) | Julia             | Broader ecosystem around Catlab for scientific computing with category theory.                                       | Agent-based modeling, differential equations, epidemiological modeling, Petri nets                          | [algebraicjulia.org](<https://www.algebraicjulia.org/>)                                                                      |

### Relational/Formal Specification Tools (Broader Family)

| Project            | Language | Description                                                                                            | Key Features                                                                                                          | Link                                                                                                         |
|--------------------|----------|--------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------|
| **Alloy Analyzer** | Java     | The most well-known lightweight formal methods tool. Relational logic + bounded model finding via SAT. | Signatures/relations, SAT-based Kodkod engine, bounded scope checking, graphical counterexamples, temporal logic (v6) | [alloytools.org](<https://alloytools.org/>) / [GitHub](<https://github.com/AlloyTools/org.alloytools.alloy>) |

### Theoretical Foundations

| Work                                                 | Author(s)      | Description                                                                                                                    | Link                                                                                                                           |
|------------------------------------------------------|----------------|--------------------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------|
| *Geometric Logic as a Specification Language* (1994) | Steven Vickers | Seminal paper proposing geometric logic as the basis for a Z-like specification language. The intellectual ancestor of Geolog. | [Springer](<https://link.springer.com/chapter/10.1007/978-1-4471-3503-6_4>) / [PDF](<http://www.cs.bham.ac.uk/~sjv//GeoZ.pdf>) |
| *Geometric Logic in Computer Science* (1993)         | Steven Vickers | Introduction to geometric logic, categorical logic, toposes, and their applications in computer science.                       | [Springer](<https://link.springer.com/chapter/10.1007/978-1-4471-3503-6_4>)                                                    |

---

### What Makes Geolog Distinctive

Compared to the above projects, Geolog combines several features that no single existing tool offers together:

* **Typed theories with geometric axioms** (like Chase/Razor) but with a richer **sort/function/relation** vocabulary (closer to Catlab)
* **Dependent/parameterized theories** — theories can take instances of other theories as parameters (e.g. `theory (N : PetriNet instance) Marking`)
* **Nested instances** — instances can contain instances of parameterized theories inline
* **Chase + equality saturation** — not just model finding but collapsing equivalent terms (as in the Category example)
* **Persistent, append-only storage** with version control — designed as infrastructure, not just a one-shot tool
* **Interactive REPL** — explore and mutate instances dynamically, unlike batch-mode model finders
* **Constructive proof witnesses** — the Petri net showcase demonstrates solutions as typed diagrammatic objects, not just boolean answers

## Changelog

* **Feb 27, 2026** -- The first version was created.