MetiTarski: An Automatic Prover for the Elementary Functions

DOI10.1007/978-3-540-85110-3_18MaRDI QIDQ5505501zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Behzad Akbarpour, Lawrence C. Paulson

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_18

Mathematics Subject Classification ID

Recommendations

• MetiTarski: An automatic theorem prover for real-valued special functions
• MetiTarski: past and future
• Real Algebraic Strategies for MetiTarski Proofs
• Extending a Resolution Prover for Inequalities on Elementary Functions
• MetiTarski's menagerie of cooperating systems

Cites work

• scientific article; zbMATH DE number 1302474 (Why is no real title available?)
• scientific article; zbMATH DE number 1349647 (Why is no real title available?)
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Automated Deduction – CADE-20
• Automatic derivation of the irrationality of \(e\)
• Extending a Resolution Prover for Inequalities on Elementary Functions
• QEPCAD B
• Resolution theorem proving
• Verified Real Number Calculations: A Library for Interval Arithmetic

Cited in

(18)

• Applications of MetiTarski in the Verification of Control and Hybrid Systems
• MetiTarski: An automatic theorem prover for real-valued special functions
• Applications of real number theorem proving in PVS
• A heuristic prover for real inequalities
• MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
• A heuristic prover for real inequalities
• A procedure for proving special function inequalities involving a discrete parameter
• scientific article; zbMATH DE number 1670744 (Why is no real title available?)
• Combining logical and algebraic techniques for natural style proving in elementary analysis
• Computer algebra for special function inequalities
• MetiTarski
• MetiTarski: past and future
• A heuristic prover for elementary analysis in \textit{Theorema}
• Metamath Zero: designing a theorem prover prover
• scientific article; zbMATH DE number 4155932 (Why is no real title available?)
• MetiTarski's menagerie of cooperating systems
• Automated proving for a class of transcendental-polynomial inequalities
• Extending a Resolution Prover for Inequalities on Elementary Functions

Describes a project that uses

Uses Software

• QEPCAD
• OTTER
• SPASS+T

This page was built for publication: MetiTarski: An Automatic Prover for the Elementary Functions

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