MetiTarski: An automatic theorem prover for real-valued special functions
From MaRDI portal
Publication:972422
DOI10.1007/s10817-009-9149-2zbMath1215.68206OpenAlexW2008288068WikidataQ30054495 ScholiaQ30054495MaRDI QIDQ972422
Behzad Akbarpour, Lawrence Charles 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
Related Items
Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems, Deadness and how to disprove liveness in hybrid dynamical systems, SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Learning theorem proving components, Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation), A logarithmic inequality, Proving tight bounds on univariate expressions with elementary functions in Coq, Case splitting in an automatic theorem prover for real-valued special functions, Isolating all the real roots of a mixed trigonometric-polynomial, Proof certificates in PVS, Fuzzy answer set computation via satisfiability modulo theories, An augmented MetiTarski dataset for real quantifier elimination using machine learning, Polynomial function intervals for floating-point software verification, Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL, Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1, Deductive verification of floating-point Java programs in KeY, A search-based procedure for nonlinear real arithmetic, Quasi-decidability of a fragment of the first-order theory of real numbers, HOL(y)Hammer: online ATP service for HOL Light, On Transfinite Knuth-Bendix Orders, A conflict-driven solving procedure for poly-power constraints, Validating QBF Validity in HOL4, Proving Valid Quantified Boolean Formulas in HOL Light, Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition, Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants, Implicit definitions with differential equations for KeYmaera X (system description), Formal Proofs for Nonlinear Optimization, Formalization of Bernstein polynomials and applications to global optimization, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
Cites Work
- Applications of real number theorem proving in PVS
- Semidefinite programming relaxations for semialgebraic problems
- Extending a Resolution Prover for Inequalities on Elementary Functions
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- The rational numbers as an abstract data type
- Applications of MetiTarski in the Verification of Control and Hybrid Systems
- Term Rewriting and All That
- QEPCAD B
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Efficient and Reliable Multiprecision Implementation of Elementary and Special Functions
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- MetiTarski: An Automatic Prover for the Elementary Functions
- Hybrid Systems: Computation and Control
- Symbolic reachability computation for families of linear vector fields
- Automatic derivation of the irrationality of \(e\)
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
