Applications of real number theorem proving in PVS
DOI10.1007/S00165-012-0232-9zbMATH Open1298.68252OpenAlexW2074445571WikidataQ55393267 ScholiaQ55393267MaRDI QIDQ469367FDOQ469367
Olga Lightfoot, Hanne Gottliebsen, Ursula Martin Webb, Ruth Hardy
Publication date: 10 November 2014
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-012-0232-9
Recommendations
- Theorem Proving in Higher Order Logics
- Real Number Calculations and Theorem Proving
- scientific article; zbMATH DE number 1259143
- Using theory interpretation to mechanise the reals in a theorem prover
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
control systemsMapleair traffic controlhigher order theorem provingPVSreal number theorem provingtest suite
Specification and verification (program logics, model checking, etc.) (68Q60) Application models in control theory (93C95)
Cites Work
- MetiTarski: An Automatic Prover for the Elementary Functions
- Title not available (Why is that?)
- Title not available (Why is that?)
- QEPCAD B
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Model theory and exponentiation.
- Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings
- Title not available (Why is that?)
- The Four Colour Theorem: Engineering of a Formal Proof
- Title not available (Why is that?)
- Title not available (Why is that?)
- A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
- Theorem Proving in Higher Order Logics
Cited In (4)
Uses Software
This page was built for publication: Applications of real number theorem proving in PVS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q469367)
