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 25 articles )
Showing results 1 to 20 of 25.
Sorted by year (- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
- 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)
- 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)
- Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
- Oostdijk, Martijn Diederik: Generation and presentation of formal mathematical documents (2001)
- Sutcliffe, Geoff; Suttner, Christian: Evaluating general purpose automated theorem proving systems (2001)
- Armando, Alessandro; Coglio, Alessandro; Giunchiglia, Fausto: The control component of open mechanized reasoning systems (1999)
- Melis, E.; Siekmann, J.: Knowledge-based proof planning (1999)