MetiTarski
From MaRDI portal
Software:13328
No author found.
Related Items (51)
Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ A heuristic prover for real inequalities ⋮ Deadness and how to disprove liveness in hybrid dynamical systems ⋮ Recent Advances in Real Geometric Reasoning ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Learning theorem proving components ⋮ Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers ⋮ Real Algebraic Strategies for MetiTarski Proofs ⋮ Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) ⋮ Pegasus: sound continuous invariant generation ⋮ A logarithmic inequality ⋮ MetiTarski: Past and Future ⋮ Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Case splitting in an automatic theorem prover for real-valued special functions ⋮ Proof certificates in PVS ⋮ Fuzzy answer set computation via satisfiability modulo theories ⋮ Polynomial function intervals for floating-point software verification ⋮ Transcendental inductive invariants generation for non-linear differential and hybrid systems ⋮ Applications of real number theorem proving in PVS ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Cylindrical algebraic sub-decompositions ⋮ 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 ⋮ Using machine learning to improve cylindrical algebraic decomposition ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ 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 ⋮ Truth table invariant cylindrical algebraic decomposition ⋮ Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition ⋮ Applications of MetiTarski in the Verification of Control and Hybrid Systems ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ Validating QBF Validity in HOL4 ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ Automated theorem proving for special functions ⋮ Cylindrical algebraic decomposition with equational constraints ⋮ The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree ⋮ Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition ⋮ Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition ⋮ Certification of Bounds of Non-linear Functions: The Templates Method ⋮ Automated Reasoning Service for HOL Light ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ MetiTarski’s Menagerie of Cooperating Systems ⋮ 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}\) ⋮ Generating invariants for non-linear hybrid systems ⋮ A Heuristic Prover for Real Inequalities
This page was built for software: MetiTarski
