Applications of real number theorem proving in PVS
From MaRDI portal
Publication:469367
DOI10.1007/s00165-012-0232-9zbMath1298.68252OpenAlexW2074445571WikidataQ55393267 ScholiaQ55393267MaRDI QIDQ469367
Olga Lightfoot, Hanne Gottliebsen, Ruth Hardy, Ursula Martin Webb
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
control systemsMapleair traffic controlhigher order theorem provingPVSreal number theorem provingtest suite
Application models in control theory (93C95) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (2)
MetiTarski: An automatic theorem prover for real-valued special functions ⋮ Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
Uses Software
Cites Work
- Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings
- The Four Colour Theorem: Engineering of a Formal Proof
- A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
- QEPCAD B
- Theorem Proving in Higher Order Logics
- MetiTarski: An Automatic Prover for the Elementary Functions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Applications of real number theorem proving in PVS
