swMATH10478MaRDI QIDQ22439FDOQ22439
Author name not available (Why is that?)
Official website: http://andrej.com/analytica/
Cited In (47)
- Hidden verification for computational mathematics
- Automatic derivation of the irrationality of \(e\)
- Foundations of Software Science and Computation Structures
- On the role of OpenMath in interactive mathematical documents
- Title not available (Why is that?)
- Exploring abstract algebra in constructive type theory
- Generation and presentation of formal mathematical documents
- Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates
- ProofWidgets
- Analytica --- an experiment in combining theorem proving and symbolic computation
- Extending a Resolution Prover for Inequalities on Elementary Functions
- A formal framework for managing mathematics
- Title not available (Why is that?)
- A heuristic prover for elementary analysis in \textit{Theorema}
- A fully automatic theorem prover with human-style output
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Formal and efficient primality proofs by use of computer algebra oracles
- MetiTarski: An automatic theorem prover for real-valued special functions
- Title not available (Why is that?)
- Enabling symbolic and numerical computations in HOL Light
- A Skeptic's approach to combining HOL and Maple
- A comparison of tools for teaching formal software verification
- Integrating computer algebra into proof planning
- Theorema
- Evaluating general purpose automated theorem proving systems
- Knowledge-based proof planning
- MetiTarski's menagerie of cooperating systems
- EAT
- IMPS
- VSDITLU
- LEGO
- CtCoq
- PROSPER
- Mathpert
- Emacs
- EVES
- Omega-MKRP
- PROVERB
- CoDe
- Mathematical Knowledge Management
- A bi-directional extensible interface between Lean and Mathematica
- An overview of a formal framework for managing mathematics
- Duration consistency filtering for qualitative simulation
- IMPS: An interactive mathematical proof system
- Modelling algebraic structures and morphisms in ACL2
- The control layer in open mechanized reasoning systems: Annotations and tactics
- Title not available (Why is that?)
This page was built for software: Analytica
