swMATH573MaRDI QIDQ13328FDOQ13328
Author name not available (Why is that?)
Official website: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-January/msg00109.html
Cited In (93)
- FPTaylor
- Deadness and how to disprove liveness in hybrid dynamical systems
- Validating QBF Validity in HOL4
- Deductive verification of floating-point Java programs in KeY
- Learning theorem proving components
- Pegasus: sound continuous invariant generation
- MetiTarski's menagerie of cooperating systems
- A conflict-driven solving procedure for poly-power constraints
- Proving Valid Quantified Boolean Formulas in HOL Light
- Recent advances in real geometric reasoning
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- 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)
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Using machine learning to improve cylindrical algebraic decomposition
- 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
- Cylindrical algebraic decomposition with equational constraints
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Automated theorem proving for special functions: the next phase
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- A heuristic prover for real inequalities
- A heuristic prover for real inequalities
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- 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)
- Generating invariants for non-linear hybrid systems
- MetiTarski: An automatic theorem prover for real-valued special functions
- Transcendental inductive invariants generation for non-linear differential and hybrid systems
- Polynomial function intervals for floating-point software verification
- QEPCAD
- RealPaver
- Benchmarks
- Gappa
- SPASS+T
- Orbital library
- Flocq
- dReal
- HSolver
- Applications of real number theorem proving in PVS
- AQCS
- Real Algebraic Strategies for MetiTarski Proofs
- Intsolver
- PolyPaver
- VSDITLU
- Squolem
- ProjectionCAD
- Analytica
- Sollya
- Manip
- PVSio
- CArL
- TopDeg
- SDeval
- Proving tight bounds on univariate expressions with elementary functions in Coq
- FloPoCo
- EFSMT
- JBernstein
- LySHA
- Stabhyli
- ABsolver
- LoAT
- Bellerophon
- BranchCuts
- Theoryguru
- Algebraic Numbers
- Girth-Chromatic
- Automated reasoning service for HOL Light
- VeriPhy
- Differential_Game_Logic
- CylindricalAlgebraicDecompose
- fasp2smt
- Special_Function_Bounds
- Cylindrical algebraic sub-decompositions
- PRECiSA
- HOL(y)Hammer: online ATP service for HOL Light
- KeYmaera X
- 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
- Decidability of univariate real algebra with predicates for rational and integer powers
- Proof certificates in PVS
- Certification of bounds of non-linear functions: the templates method
- MetiTarski: past and future
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- A search-based procedure for nonlinear real arithmetic
- Proof pearl: a probabilistic proof for the girth-chromatic number theorem
- On transfinite Knuth-Bendix orders
This page was built for software: MetiTarski
