MetiTarski: An automatic theorem prover for real-valued special functions
From MaRDI portal
Publication:972422
Recommendations
- MetiTarski: An Automatic Prover for the Elementary Functions
- Automated theorem proving for special functions: the next phase
- scientific article; zbMATH DE number 4155932
- 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
- scientific article; zbMATH DE number 3863589 (Why is no real title available?)
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 3824309 (Why is no real title available?)
- scientific article; zbMATH DE number 3176962 (Why is no real title available?)
- scientific article; zbMATH DE number 1302474 (Why is no real title available?)
- scientific article; zbMATH DE number 1349647 (Why is no real title available?)
- scientific article; zbMATH DE number 5263038 (Why is no real title available?)
- scientific article; zbMATH DE number 3338292 (Why is no real title available?)
- scientific article; zbMATH DE number 2243090 (Why is no real title available?)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Applications of MetiTarski in the Verification of Control and Hybrid Systems
- Applications of real number theorem proving in PVS
- Automated Deduction – CADE-20
- Automatic derivation of the irrationality of \(e\)
- Efficient and Reliable Multiprecision Implementation of Elementary and Special Functions
- Extending a Resolution Prover for Inequalities on Elementary Functions
- 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
- Hybrid Systems: Computation and Control
- MetiTarski: An Automatic Prover for the Elementary Functions
- Problems in mathematical analysis II. Continuity and differentiation. Transl. from the Polish, revised and augmented by the authors
- QEPCAD B
- Resolution theorem proving
- Semidefinite programming relaxations for semialgebraic problems
- Symbolic reachability computation for families of linear vector fields
- Term Rewriting and All That
- The rational numbers as an abstract data type
- Theorem Proving in Higher Order Logics
- Verified Real Number Calculations: A Library for Interval Arithmetic
Cited in
(41)- Implicit definitions with differential equations for KeYmaera X (system description)
- Quasi-decidability of a fragment of the first-order theory of real numbers
- A conflict-driven solving procedure for poly-power constraints
- Deductive verification of floating-point Java programs in KeY
- Learning theorem proving components
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
- A logarithmic inequality
- Proof certificates in PVS
- scientific article; zbMATH DE number 1670744 (Why is no real title available?)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Iscalc: An Interactive Symbolic Computation Framework (System Description)
- Proving Valid Quantified Boolean Formulas in HOL Light
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- On transfinite Knuth-Bendix orders
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Case splitting in an automatic theorem prover for real-valued special functions
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- MetiTarski: past and future
- Fuzzy answer set computation via satisfiability modulo theories
- Automated theorem proving for special functions: the next phase
- A heuristic prover for elementary analysis in \textit{Theorema}
- MetiTarski: An Automatic Prover for the Elementary Functions
- A search-based procedure for nonlinear real arithmetic
- Validating QBF Validity in HOL4
- Formalization of Bernstein polynomials and applications to global optimization
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Formal Proofs for Nonlinear Optimization
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- HOL(y)Hammer: online ATP service for HOL Light
- An augmented MetiTarski dataset for real quantifier elimination using machine learning
- MetiTarski's menagerie of cooperating systems
- Analytica -- an experiment in combining theorem proving and symbolic computation
- Deadness and how to disprove liveness in hybrid dynamical systems
- Polynomial function intervals for floating-point software verification
- Isolating all the real roots of a mixed trigonometric-polynomial
- Extending a Resolution Prover for Inequalities on Elementary Functions
- An interpreter for quantum circuits
Describes a project that uses
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)
