Applications of real number theorem proving in PVS

DOI10.1007/S00165-012-0232-9MaRDI QIDQ469367zbMATH OpenOpenAlexWikidataFDO

Authors Hanne Gottliebsen, Ruth Hardy, Olga Lightfoot, 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

zbMATH Keywords

control systemsMapleair traffic controlhigher order theorem provingPVSreal number theorem provingtest suite

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Application models in control theory (93C95)

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

Cites work

• scientific article; zbMATH DE number 1670737 (Why is no real title available?)
• scientific article; zbMATH DE number 1670746 (Why is no real title available?)
• scientific article; zbMATH DE number 3706504 (Why is no real title available?)
• scientific article; zbMATH DE number 53583 (Why is no real title available?)
• scientific article; zbMATH DE number 3548474 (Why is no real title available?)
• scientific article; zbMATH DE number 1254246 (Why is no real title available?)
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 1341611 (Why is no real title available?)
• scientific article; zbMATH DE number 1863375 (Why is no real title available?)
• scientific article; zbMATH DE number 3232102 (Why is no real title available?)
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• MetiTarski: An Automatic Prover for the Elementary Functions
• Model theory and exponentiation.
• QEPCAD B
• The Four Colour Theorem: Engineering of a Formal Proof
• Theorem Proving in Higher Order Logics
• Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings

Cited in

(5)

• MetiTarski: An automatic theorem prover for real-valued special functions
• Theorem Proving in Higher Order Logics
• Real Number Calculations and Theorem Proving
• Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
• Elements of mathematical analysis in PVS

Describes a project that uses

Uses Software

• Maple
• Matlab
• MetiTarski
• QEPCAD
• Isabelle/HOL
• PVS
• Simulink
• Automath
• VSDITLU
• Flyspeck

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)