MetiTarski

The orcale metit integrates the MetiTarski theorem prover as a trusted external decision procedure into the PVS theorem prover. The oracle 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.

Downloads

• The oracle metit is available as part of the NASA PVS Library.
• Examples.

Publications

• William Denman and César Muñoz, Automated Real Proving in PVS via MetiTarski, Proceedings of the 19th International Symposium on Formal Methods (FM 2014), Lecture Notes in Computer Science, Vol. 8442, pp. 194-199, 2014. BibTeX Reference.

The tag identifies links that are outside the NASA domain