Axiom calls COQ (for Spad code) and ACL2 (for Lisp code) at build time
in order to run proofs. It is hard enough trying to construct proofs by hand
despite the notion that Spad is "nearly mathematical". Implementation
details matter a lot. We do, however, have the types already available.
Even with
Sorry – I’ve not been much involved: other projects. But I just saw this –
haven’t looked in any detail yet.
DeepAlgebra - an outline of a program
Authors: Przemyslaw Chojecki
Categories: cs.AI math.AG
Comments: 6 pages, https://przchojecki.github.io/deepalgebra/
\\
We outline a program in
