Automated Real Proving in PVS via MetiTarskiThis paper reports the development of a proof strategy that integrates the MetiTarski theorem prover as a trusted external decision procedure into the PVS theorem prover. The strategy automatically discharges PVS sequents containing real-valued formulas, including transcendental and special functions, by translating the sequents into first order formulas and submitting them to MetiTarski. The new strategy is considerably faster and more powerful than other strategies for nonlinear arithmetic available to PVS.
Document ID
20140006393
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Denman, William (Cambridge Univ. Cambridge, United Kingdom)
Munoz, Cesar (NASA Langley Research Center Hampton, VA, United States)
Date Acquired
May 28, 2014
Publication Date
May 12, 2014
Subject Category
Numerical Analysis
Report/Patent Number
NF1676L-17715
Meeting Information
Meeting: International Symposium on Formal Methods