Lightweight integration of the Ergo theorem prover inside a proof assistant

Proceedings of the second workshop on Automated formal methods, pp. 55-59, 2007.

Cited by: 22|Bibtex|Views0|Links
EI
Keywords:
ergo theorem proverlightweight integrationsound integrationuninterpreted symbolnew combination schemeMore(12+)

Abstract:

Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Er...More

Code:

Data:

Your rating :
0

 

Tags
Comments