3 ms·

Is there an existing CAS built on top of a SAT or SMT solver?

• mathisfun123 3y ago
  oss? none that i'm aware of that use a SAT/SMT solver for the term rewriting (like i'm suggesting). closed source, my strong intuition is both mathematica and magma work this way.
  • abecedarius 3y ago
    Sounds like a great project idea to make a toy demo of this direction you'd like to see. Maybe comparable to https://github.com/norvig/paip-lisp/blob/main/docs/chapter15.md https://github.com/norvig/paip-lisp/blob/main/docs/chapter15... and https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.md https://github.com/norvig/paip-lisp/blob/main/docs/chapter8.... which are a few hundred lines of Lisp each, but do enough to be interesting.
  • deleted 3y ago
    [deleted]