Analytica --- an experiment in combining theorem proving and symbolic computation
From MaRDI portal
Publication:1272608
DOI10.1023/A:1006079212546zbMath0916.68143OpenAlexW1544772966MaRDI QIDQ1272608
Andrej Bauer, Xudong Zhao, Edmund M. Clarke
Publication date: 29 June 1999
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1006079212546
Related Items
A heuristic prover for elementary analysis in \textit{Theorema}, Enabling Symbolic and Numerical Computations in HOL Light, A bi-directional extensible interface between Lean and Mathematica, Hidden verification for computational mathematics, Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates, MBase: Representing knowledge and context for the integration of mathematical software systems, Combining symbolic computation and theorem proving: Some problems of Ramanujan, Modelling algebraic structures and morphisms in ACL2, Evaluating general purpose automated theorem proving systems
Uses Software
