Crate razor_chase

Rusty Razor is a tool for constructing finite models for first-order theories with equality.

The model-finding algorithm is inspired by the Chase in database systems. Given an input first-order theory, Razor constructs a set of homomorphically minimal models that satisfy theory.

To learn more about the theoretical foundation of Razor, check out my PhD dissertation.

Modules

• chase
  Provides a framework and interfaces to various components that are used for implementing the Chase. It also implements entrypoints for running the Chase.
• trace