Integrating SVC and HOL with the PROSPER Toolkit

Stevenson, Alan; Dennis, Louise Abigail

Abstract

We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit.
The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexamples and a framework has been devised for handling counterexamples in a HOL setting.

Citation

Stevenson, A., & Dennis, L. A. Integrating SVC and HOL with the PROSPER Toolkit. Presented at Theorem Proving in Higher Order Logics (TPHOLs 2000) Supplemental Proceedings

• Conference Name: Theorem Proving in Higher Order Logics (TPHOLs 2000) Supplemental Proceedings
• Publication Date: Jan 1, 2000
• Deposit Date: Dec 8, 2005
• Publicly Available Date: Oct 9, 2007
• Peer Reviewed: Not Peer Reviewed
• Public URL: https://nottingham-repository.worktribe.com/output/1023771
• Additional Information: Published in OGI Technical Report CSE 00-009