MetiTarski: An automatic theorem prover for real-valued special functions

DOI10.1007/S10817-009-9149-2MaRDI QIDQ972422zbMATH OpenOpenAlexWikidataFDO

Authors Behzad Akbarpour, Lawrence C. Paulson

Publication date 26 May 2010

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9149-2

zbMATH Keywords

resolution theorem prover

Mathematics Subject Classification ID

Recommendations

• MetiTarski: An Automatic Prover for the Elementary Functions
• Automated theorem proving for special functions: the next phase
• scientific article; zbMATH DE number 4155932
• Case splitting in an automatic theorem prover for real-valued special functions
• System of automation of proving theorems of the theory of metanominative data
• Real Algebraic Strategies for MetiTarski Proofs
• Metamath Zero: designing a theorem prover prover
• M-calculus -- a sequent method for automatic theorem proving
• Foundations of a theorem prover for functional and mathematical uses

Cites work

• scientific article; zbMATH DE number 3863589 (Why is no real title available?)
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3824309 (Why is no real title available?)
• scientific article; zbMATH DE number 3176962 (Why is no real title available?)
• scientific article; zbMATH DE number 1302474 (Why is no real title available?)
• scientific article; zbMATH DE number 1349647 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• scientific article; zbMATH DE number 3338292 (Why is no real title available?)
• scientific article; zbMATH DE number 2243090 (Why is no real title available?)
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Applications of MetiTarski in the Verification of Control and Hybrid Systems
• Applications of real number theorem proving in PVS
• Automated Deduction – CADE-20
• Automatic derivation of the irrationality of e
• Efficient and Reliable Multiprecision Implementation of Elementary and Special Functions
• Extending a Resolution Prover for Inequalities on Elementary Functions
• Handbook of continued fractions for special functions. With contributions by Franky Backeljauw and Catherine Bonan-Hamada. Verified numerical output by Stefan Becuwe and Annie Cuyt
• Hybrid Systems: Computation and Control
• MetiTarski: An Automatic Prover for the Elementary Functions
• Problems in mathematical analysis II. Continuity and differentiation. Transl. from the Polish, revised and augmented by the authors
• QEPCAD B
• Resolution theorem proving
• Semidefinite programming relaxations for semialgebraic problems
• Symbolic reachability computation for families of linear vector fields
• Term Rewriting and All That
• The rational numbers as an abstract data type
• Theorem Proving in Higher Order Logics
• Verified Real Number Calculations: A Library for Interval Arithmetic

Describes a project that uses

Uses Software

• Analytica
• HSolver
• SLEEF
• SPASS+T
• RSOLVER
• OTTER
• HySAT
• QEPCAD
• MetiTarski

This page was built for publication: MetiTarski: An automatic theorem prover for real-valued special functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q972422)