alg
alg copied to clipboard
andrejbauer
Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.
For the following file: ``` Axiom: (forall x, True). ``` I get the error: ``` Syntax error at line 0, characters 8-14: I got confused here ``` In particular, alg...
Quantale distributivity laws were incorrect. Bottom element preservation requirements were missing.
The Makefile depends on ocamlbuild, but instructions only install ocaml and menhir.
Binaries are currently not available on the website http://math.andrej.com/alg/. Can I suggest that you use GitHub releases to host them? I found this very convenient for my projects. P.S.: Thank...
This commit introduces racks and quandles. Besides that, it makes other theories consistent.
Why do we have `eval` functions in `eval.ml` as well as in `first_order.ml`?
It seems that `eventual_period` in `unary_invariant` and `binary_invariant` is needlessly quadratic time. If we keep track of _when_ we saw each element, then when an element re-appears, we will instantly...
Abstract sytnax does not keep the source code locations. This is bad because error reporting cannot give information about where an error occurred.
It looks like alg used menhir from the very start. I suggest we keep using it. We'll provide binaries for people on Windows anyway.
Metadata
Owner
Metadata
Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.