Salman Saghafi

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).

Supporting differential views (containing `Difference` expressions) requires support for negative increments of tuples (negative deltas) for incremental view maintenance. The code explicitly prohibits differential views in `database::validate::ViewExpressionValidator`.