Expand description
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.