Extending a Resolution Prover for Inequalities on Elementary Functions

DOI10.1007/978-3-540-75560-9_6zbMath1137.68571OpenAlexW1598448873MaRDI QIDQ3498456

Behzad Akbarpour, Lawrence Charles Paulson

Publication date: 15 May 2008

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-75560-9_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (8)

A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper) ⋮ Real Number Calculations and Theorem Proving ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ Real World Verification ⋮ Applications of MetiTarski in the Verification of Control and Hybrid Systems ⋮ MetiTarski: An Automatic Prover for the Elementary Functions ⋮ Combining Isabelle and QEPCAD-B in the Prover’s Palette

Uses Software

• QEPCAD
• Isabelle/HOL
• OTTER
• Metis_
• SPASS+T
• Analytica

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• QEPCAD B
• A formally verified proof of the prime number theorem
• Combining decision procedures for the reals
• Automated Deduction – CADE-20
• Theorem Proving in Higher Order Logics
• Computer Aided Verification
• Automatic derivation of the irrationality of \(e\)

This page was built for publication: Extending a Resolution Prover for Inequalities on Elementary Functions