A SAT solver based calculator for discrete mathematics and universal algebra.
- Formulas: first order sentences on multiple domains (tensors, no power set)
- Small structures: elements are integers, operations and relations are tensors
- Large structures: elements are tensors, operations and relations are formulas
- Turn large structures into small ones using SAT solver
- Subalgebra/congruence lattice of small algebras is a large meet semilattice
- Find meet irreducible elements of large meet semilattice, get large lattice
- Turn large Galois connection (clones) into a small Galois connection
- Varieties: signature, axioms, theorems, ability to verify on structures
- Polymorphic large structures (parameterized by integers, maybe by tensors)