rusty-razor
rusty-razor copied to clipboard
salmans
Razor is a tool for constructing finite models for first-order theories
When passing an input file with `.md` extension as the input theory, Razor parses all code blocks between ``` for the input theory. @ramsdell tagging you here for tracking
1. How does Alloy's bounds translate to Razor's? 2. Maybe the comparison should be done after implementing sorted logic for Razor?
The existing implementations of `StrategyTrait` do not take advantage of information about the previously evaluated sequents. ## Definitions *Unbalanced Sequent:* is a sequent whose body is true in the model...
There are some obvious choices: - [ ] JSON - [ ] S-Expression
The core idea is to avoid introducing new elements to the model when possible. Here is an example for the simple case: ``` P('a); exists x. P(x); ``` Razor currently...
Collecting some thoughts: * Sorted chase seems to be pretty straight forward * Sorted chase would dramatically improve performance (restricting the possible ways of instantiating sequents) * Requires change in...
This must be done as a separate tool, using Razor's syntactic library.
See http://www.tptp.org The goal is to use the TPTP library as test cases. A TPTP parser must be developed as a separate project. Consider LALRPOP as an option (https://github.com/salmans/rusty-razor/issues/40).
CNF and DNF data structures now support quantifiers (universal and existential), followed by a matrix in normal form. This allows for converting to CNF/DNF without Skolemization, which is needed for...