Analytica
Analytica: A theorem prover for Mathematica. Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in Mathematica language and runs in the Mathematica environment. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to guarantee the correctness of certain steps that are made by the symbolic computation system and therefore prevent common errors like division by a symbolic expression that could be zero. In this paper we describe the structure of Analytica and explain the main techniques that it uses to construct proofs. We have tried to make the paper as self-contained as possible so that it will be accessible to a wide audience of potential users. ...
Keywords for this software
References in zbMATH (referenced in 31 articles )
Showing results 1 to 20 of 31.
Sorted by year (- Ganesalingam, M.; Gowers, W. T.: A fully automatic theorem prover with human-style output (2017)
- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
- Seddiki, Ons; Dunchev, Cvetan; Khan-Afshar, Sanaz; Tahar, Sofiène: Enabling symbolic and numerical computations in HOL Light (2015)
- Paulson, Lawrence C.: MetiTarski’s menagerie of cooperating systems (2013)
- Akbarpour, Behzad; Paulson, Lawrence Charles: MetiTarski: An automatic theorem prover for real-valued special functions (2010)
- Feinerer, Ingo; Salzer, Gernot: A comparison of tools for teaching formal software verification (2009)
- Akbarpour, Behzad; Paulson, Lawrence C.: Extending a resolution prover for inequalities on elementary functions (2007)
- Cantone, Domenico; Cincotti, Gianluca; Gallo, Giovanni: Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates (2006)
- Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula: Hidden verification for computational mathematics (2005)
- Kutsia, Temur; Buchberger, Bruno: Predicate logic with sequence variables and sequence function symbols (2004)
- Ramanathan, Ajith; Mitchell, John; Scedrov, Andre; Teague, Vanessa: Probabilistic bisimulation and equivalence for security analysis of network protocols (2004)
- Farmer, William M.; von Mohrenschildt, Martin: An overview of a formal framework for managing mathematics (2003)
- Könik, Tolga; Say, A. C. Cem: Duration consistency filtering for qualitative simulation (2003)
- Omodeo, Eugenio G.; Schwartz, Jacob T.: A `theory’ mechanism for a proof-verifier based on first-order set theory (2002)
- Zimmer, Jürgen; Dennis, Louise A.: Inductive theorem proving and computer algebra in the MathWeb Software Bus (2002)
- Armando, Alessandro; Coglio, Alessandro; Giunchiglia, Fausto; Ranise, Silvio: The control layer in open mechanized reasoning systems: Annotations and tactics (2001)
- Beeson, Michael: Automatic derivation of the irrationality of (e) (2001)
- Caprotti, O.; Cohen, A. M.: On the role of OpenMath in interactive mathematical documents (2001)
- Caprotti, Olga; Oostdijk, Martijn: Formal and efficient primality proofs by use of computer algebra oracles (2001)
- Farmer, William M.; von Mohrenschildt, Martin: A formal framework for managing mathematics (2001)