Extending a Resolution Prover for Inequalities on Elementary Functions
From MaRDI portal
Recommendations
Cites work
- A formally verified proof of the prime number theorem
- Automated Deduction – CADE-20
- Automatic derivation of the irrationality of e
- Combining decision procedures for the reals
- scientific article; zbMATH DE number 1302474 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- QEPCAD B
- Resolution theorem proving
- Theorem Proving in Higher Order Logics
- Theorem proving using lazy proof explication.
Cited in
(12)- Modular proof systems for partial functions with Evans equality
- A heuristic prover for real inequalities
- A heuristic prover for real inequalities
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Real Number Calculations and Theorem Proving
- Applications of MetiTarski in the Verification of Control and Hybrid Systems
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)
- Real World Verification
- MetiTarski: An Automatic Prover for the Elementary Functions
- Combining Isabelle and QEPCAD-B in the Prover’s Palette
- MetiTarski: An automatic theorem prover for real-valued special functions
This page was built for publication: Extending a Resolution Prover for Inequalities on Elementary Functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3498456)
