MetiTarski
From MaRDI portal
Software:13328
swMATH573MaRDI QIDQ13328FDOQ13328
Author name not available (Why is that?)
Cited In (51)
- Formal Proofs for Nonlinear Optimization
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Implicit definitions with differential equations for KeYmaera X (system description)
- Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Using machine learning to improve cylindrical algebraic decomposition
- Certification of Bounds of Non-linear Functions: The Templates Method
- MetiTarski: Past and Future
- Deadness and how to disprove liveness in hybrid dynamical systems
- Cylindrical algebraic decomposition with equational constraints
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Validating QBF Validity in HOL4
- Deductive verification of floating-point Java programs in KeY
- Automated theorem proving for special functions: the next phase
- 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
- A heuristic prover for real inequalities
- Recent Advances in Real Geometric Reasoning
- 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
- Generating invariants for non-linear hybrid systems
- MetiTarski: An automatic theorem prover for real-valued special functions
- Pegasus: sound continuous invariant generation
- MetiTarski’s Menagerie of Cooperating Systems
- Transcendental inductive invariants generation for non-linear differential and hybrid systems
- Polynomial function intervals for floating-point software verification
- Applications of real number theorem proving in PVS
- Real Algebraic Strategies for MetiTarski Proofs
- Proving tight bounds on univariate expressions with elementary functions in Coq
- The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree
- Cylindrical algebraic sub-decompositions
- On Transfinite Knuth-Bendix Orders
- 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
- Applications of MetiTarski in the Verification of Control and Hybrid Systems
- Truth table invariant cylindrical algebraic decomposition
- 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
- Proof certificates in PVS
- A conflict-driven solving procedure for poly-power constraints
- Automated Reasoning Service for HOL Light
- A Heuristic Prover for Real Inequalities
- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition
- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition
- A search-based procedure for nonlinear real arithmetic
- Proving Valid Quantified Boolean Formulas in HOL Light
This page was built for software: MetiTarski
