Abstract
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.
Work funded ESPRIT Framework IV Grant LTR 26241
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
References
Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The PROSPER Toolkit. In: TACAS 2000 (2000) (to appear)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
Hyvö, E., De Pascale, S.: A New Basis for Spreadsheet Computing: Interval Solver TM forMicrosoft Excel. In: Proceedings of 16th National Conference on Artificial Intelligence and 11th Innovative Applications of Artificial Intelligence Conference (AAAI/IAAI 1999), pp. 799–806. AAAI Press / The MIT Press (1999)
Microsoft Corporation, Microsoft Excel, http://www.microsoft.com/excel
Sheeran, M., Stålmarck, G.: A tutorial on stålmarck’s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)
Stålmarck, G., Säflund, M.: Modelling and Verifying Systems and Software in Propositional Logic. In: Proceedings of SAFECOMP 1990, pp. 31–36. Pergamon Press, Oxford (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collins, G., Dennis, L.A. (2000). System Description: Embedding Verification into Microsoft Excel. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_40
Download citation
DOI: https://doi.org/10.1007/10721959_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive