Formalization of the Integral Calculus in the PVS Theorem Prover

The PVS Theorem prover is a widely used formal verification tool used for the analysis of safetycritical systems. The PVS prover, though fully equipped to support deduction in a very general logic framework, namely higher-order logic, it must nevertheless, be augmented with the definitions and assoc...

Full description

Bibliographic Details
Main Author: Ricky Wayne Butler
Format: Article
Language:English
Published: University of Bologna 2009-04-01
Series:Journal of Formalized Reasoning
Online Access:http://jfr.cib.unibo.it/article/view/1349/778