The following pages link to MetiTarski (Q13328):
Displayed 50 items.
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- Polynomial function intervals for floating-point software verification (Q457251) (← links)
- Applications of real number theorem proving in PVS (Q469367) (← links)
- Cylindrical algebraic sub-decompositions (Q475412) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- MetiTarski: An automatic theorem prover for real-valued special functions (Q972422) (← links)
- A logarithmic inequality (Q1646361) (← links)
- Proof certificates in PVS (Q1687741) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Using machine learning to improve cylindrical algebraic decomposition (Q2009221) (← links)
- Quasi-decidability of a fragment of the first-order theory of real numbers (Q2013319) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- Implicit definitions with differential equations for KeYmaera X (system description) (Q2104559) (← links)
- Learning theorem proving components (Q2142080) (← links)
- Pegasus: sound continuous invariant generation (Q2147687) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (Q2287902) (← links)
- A conflict-driven solving procedure for poly-power constraints (Q2303230) (← links)
- Cylindrical algebraic decomposition with equational constraints (Q2307622) (← links)
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (Q2331077) (← links)
- Formalization of Bernstein polynomials and applications to global optimization (Q2351165) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Generating invariants for non-linear hybrid systems (Q2355695) (← links)
- Deadness and how to disprove liveness in hybrid dynamical systems (Q2629097) (← links)
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) (Q2635072) (← links)
- Automated theorem proving for special functions (Q2819703) (← links)
- The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree (Q2829999) (← links)
- Certification of Bounds of Non-linear Functions: The Templates Method (Q2843005) (← links)
- Automated Reasoning Service for HOL Light (Q2843009) (← links)
- MetiTarski’s Menagerie of Cooperating Systems (Q2849476) (← links)
- A Heuristic Prover for Real Inequalities (Q2879243) (← links)
- Real Algebraic Strategies for MetiTarski Proofs (Q2907335) (← links)
- MetiTarski: Past and Future (Q2914728) (← links)
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem (Q2914757) (← links)
- Transcendental inductive invariants generation for non-linear differential and hybrid systems (Q2986749) (← links)
- Validating QBF Validity in HOL4 (Q3088005) (← links)
- Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
- Recent Advances in Real Geometric Reasoning (Q3452275) (← links)
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (Q3453240) (← links)
- Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers (Q3454091) (← links)
- Applications of MetiTarski in the Verification of Control and Hybrid Systems (Q3624557) (← links)
- Fuzzy answer set computation via satisfiability modulo theories (Q4592999) (← links)
- Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 (Q5145435) (← links)
- Formal Proofs for Nonlinear Optimization (Q5195260) (← links)
- On Transfinite Knuth-Bendix Orders (Q5200038) (← links)
- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition (Q5495913) (← links)
- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition (Q5495916) (← links)