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
The weaver program can now process a latex document.
The end result is a tree structure of the same document.
There is still more to do, of course. Much more.
It is clear that the semantics of the markup tags are all in
the weaver program. This is obvious in hindsight since the
markup needs to be
On Sat, Aug 27, 2016 at 12:14 PM, Richard Fateman
wrote:
>
> Take up a book on complex analysis and see what problems you have
> as you try to encode the statements, or especially the homework
> problems. I tried this decades ago with the text I used,
> https://www.amazon.com/Functions-Complex-V
Designation of branch cuts is sometimes denoted by natural language.
While the end points are specific -- depend of singularities -- the
cuts can be moved for convenience, and this is done often to evaluate
contour integrals, for example.
Take up a book on complex analysis and see what problems y
(email failed...retry)
William Sit wrote:
===
>I am still not sure what your immediate goal is. My current understanding
(correct me
>if I am still wrong) is that you want to translate the left hand side of
an identity (like a
>formula for an integral) given in latex into Axiom code which the
(email failed... retry)
The referenced paper only looked at the DLMF Airy functions. The results
are:
"Of the 17 sections in the DLMF sample chapter on Airy functions we can
handle the mathematical
formulas completely in 6, partially in 5 (without the transformation to
MathML), and 6 remain
inc
