Integrating SVC and HOL with the PROSPER Toolkit
(2000)
Conference Proceeding
Stevenson, A., & Dennis, L. A. (2000). Integrating SVC and HOL with the PROSPER Toolkit.
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... Read More about Integrating SVC and HOL with the PROSPER Toolkit.