Export newly learned equalities (for interaction with other solvers)
Make detection of "impossible" work explicit (rather then using mplus)
Move variable to the external interface.
Bugfix: avoid name clashes in rule generation.
Export Var as abstract.
Avoid shadowing warnings.
Remove old proof constructors and add distributivity rules.
Remove unused module
Add all associativity rules.
Add frules instantiate with base axioms.
More improvements to closure computation.
Simplify code. Also ensures that we process equalities first.
Checkpoint (possibly broken)
Fix the impossibility tests.
Switch to new genRule system.
New genRule code is pretty much complete (but untested).
Generate code for equality closure from rules.
Cleanup and simplify genRule (not yet finished)
Program basic axioms explicitly.
This is simpler than the code to generate these automatically.
Remove the extra annotation on Num.
An attempt to eliminate the automatically generated rules.
This is not complete and parts of the code feel quite repetitive,
perhaps, some automatic generation is not such a bad idea...
Add missing axiom "forall a. 0 <= a"
Add totality axioms, which are not used at the moment.
These would justify naming things.
Some thought about how to avoid synthetic rules.
Some example proofs using the axioms.
Add axioms to makefile.
An explicit list of all axioms.
Forward monotonicity rules.
Notes on proofs of backward interval rules.
Note about monotonicity rules, justifying interval improvements.
Just some more notes.