Automated Real Proving in PVS via MetiTarski
2014
This 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
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
11
References
19
Citations
NaN
KQI