Iscalc: An Interactive Symbolic Computation Framework (System Description)

DOI10.1007/978-3-031-38499-8_33MaRDI QIDQ6492772zbMATH OpenFDO

Authors Bohua Zhan, Runqing Xu

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_33

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A bi-directional extensible interface between Lean and Mathematica
• A heuristic prover for real inequalities
• A Skeptic's approach to combining HOL and Maple
• Analytica --- an experiment in combining theorem proving and symbolic computation
• Automated and readable simplification of trigonometric expressions
• Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
• Feedback systems: an introduction for scientists and engineers.
• Formalization of real analysis: a survey of proof assistants and libraries
• MetiTarski: An automatic theorem prover for real-valued special functions
• The Lean 4 theorem prover and programming language
• The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
• Verified interactive computation of definite integrals
• Verified Real Asymptotics in Isabelle/HOL

This page was built for publication: Iscalc: An Interactive Symbolic Computation Framework (System Description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492772)