Skip to main content

Research Repository

Advanced Search

System Description: Embedding Verification into Microsoft Excel

Collins, Graham; Dennis, Louise Abigail


Graham Collins

Louise Abigail Dennis


David McAllester


The aim of the PROSPER project is to allow the embedding of existing verification technology into applications in such a way that the theorem proving is hidden, or presented to the end user in a natural way. This paper describes a system built to test whether the PROSPER toolkit satisfied this aim. The system combines the toolkit with Microsoft Excel, a popular commercial spreadsheet application.


Collins, G., & Dennis, L. A. (2000). System Description: Embedding Verification into Microsoft Excel. In D. McAllester (Ed.),

Conference Name Automted Deduction (CADE-17)
Publication Date Jan 1, 2000
Deposit Date Dec 8, 2005
Publicly Available Date Oct 9, 2007
Peer Reviewed Peer Reviewed
Public URL
Additional Information Lecture Notes in Artificial Intelligence 1831


Downloadable Citations