MetiTarski: An automatic theorem prover for real-valued special functions
From MaRDI portal
Publication:972422
DOI10.1007/S10817-009-9149-2zbMATH Open1215.68206OpenAlexW2008288068WikidataQ30054495 ScholiaQ30054495MaRDI QIDQ972422FDOQ972422
Authors: Behzad Akbarpour, Lawrence C. Paulson 
Publication date: 26 May 2010
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9149-2
Recommendations
- MetiTarski: An Automatic Prover for the Elementary Functions
- Automated theorem proving for special functions: the next phase
- scientific article
- Case splitting in an automatic theorem prover for real-valued special functions
- System of automation of proving theorems of the theory of metanominative data
- Real Algebraic Strategies for MetiTarski Proofs
- Metamath Zero: designing a theorem prover prover
- \(M\)-calculus -- a sequent method for automatic theorem proving
- Foundations of a theorem prover for functional and mathematical uses
Cites Work
- MetiTarski: An Automatic Prover for the Elementary Functions
- QEPCAD B
- Hybrid Systems: Computation and Control
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semidefinite programming relaxations for semialgebraic problems
- Resolution theorem proving
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Term Rewriting and All That
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Automated Deduction – CADE-20
- Handbook of continued fractions for special functions. With contributions by Franky Backeljauw and Catherine Bonan-Hamada. Verified numerical output by Stefan Becuwe and Annie Cuyt
- The rational numbers as an abstract data type
- Theorem Proving in Higher Order Logics
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Title not available (Why is that?)
- Title not available (Why is that?)
- Problems in mathematical analysis II. Continuity and differentiation. Transl. from the Polish, revised and augmented by the authors
- Efficient and Reliable Multiprecision Implementation of Elementary and Special Functions
- Title not available (Why is that?)
- Symbolic reachability computation for families of linear vector fields
- Applications of real number theorem proving in PVS
- Applications of MetiTarski in the Verification of Control and Hybrid Systems
- Automatic derivation of the irrationality of \(e\)
Cited In (37)
- Formal Proofs for Nonlinear Optimization
- Title not available (Why is that?)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Implicit definitions with differential equations for KeYmaera X (system description)
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Deadness and how to disprove liveness in hybrid dynamical systems
- Validating QBF Validity in HOL4
- Deductive verification of floating-point Java programs in KeY
- An interpreter for quantum circuits
- Extending a Resolution Prover for Inequalities on Elementary Functions
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Isolating all the real roots of a mixed trigonometric-polynomial
- A logarithmic inequality
- Fuzzy answer set computation via satisfiability modulo theories
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Learning theorem proving components
- Polynomial function intervals for floating-point software verification
- Proving tight bounds on univariate expressions with elementary functions in Coq
- MetiTarski: An Automatic Prover for the Elementary Functions
- Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1
- HOL(y)Hammer: online ATP service for HOL Light
- Iscalc: An Interactive Symbolic Computation Framework (System Description)
- Case splitting in an automatic theorem prover for real-valued special functions
- Formalization of Bernstein polynomials and applications to global optimization
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Quasi-decidability of a fragment of the first-order theory of real numbers
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
- Proof certificates in PVS
- A conflict-driven solving procedure for poly-power constraints
- MetiTarski: past and future
- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition
- A search-based procedure for nonlinear real arithmetic
- An augmented MetiTarski dataset for real quantifier elimination using machine learning
- Proving Valid Quantified Boolean Formulas in HOL Light
- On transfinite Knuth-Bendix orders
Uses Software
This page was built for publication: MetiTarski: An automatic theorem prover for real-valued special functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q972422)
