Abstract
In this paper we present the higher-order logic used in theorem-provers like the HOL system (see [GM 93]) or Isabelle HOL logic (see [Paul 94]) as an institution. Then we show that for maps of institutions into HOL that satisfy certain technical conditions we can reuse the proof system of the higher-order logic to reason about structured specifications built over the institutions mapped into HOL. We also show some maps of institutions underlying the CASL specification formalism (see [CASL 99]) into HOL that satisfy conditions needed for reusing proof systems.
This research was partially supported by ESPRIT CRIT2 program, working group 29432 (CoFI WG) and KBN grant 8 T11C 037 16.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andrews, P.B.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, INC., London (1986)
Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics. Studies in Logic and The Foundations of Mathematics. Elsevier, Amsterdam (1998)
Borzyszkowski, T.: Moving specification structures between logical systems. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 16–28. Springer, Heidelberg (1998)
Borzyszkowski, T.: Logical systems for structured specifications. Special issue of Theoretical Computer Science (to appear), See http://monika.univ.gda.pl/~mattb/papers.html
CASL The Common Algebraic Specification Language - Summary, by The CoFI Task Group on Language Design. Version 1.0 (March 19, 1999), Document is available on http://www.brics.dk/Projects/CoFI/Notes/S-9/ and ftp://ftp.brics.dk/Projects/CoFI/Notes/S-9/
Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Undergraduate Texts in Mathematics. Springer, Heidelberg (1996)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specifications and programming. Journal of the Assoc. for Computing Machinery 39, 95–146 (1992)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)
Meseguer, J.: General logic. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium 1987, pp. 279–329. North-Holland, Amsterdam (1989)
Mossakowski, T., Kolyang, Krieg-Brückner, B.: Static Semantic Analysis and Theorem Proving for CASL. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, Springer, Heidelberg (1998)
Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Sannella, D., SokoGlowski, S., Tarlecki, A.: Towards formal development of programs from algebraic specification: parameterization revisited. Acta Informatica 29, 689–736 (1992)
Tarlecki, A.: Moving between logical systems. Recent Trends in Data Type Specifications. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
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
Borzyszkowski, T. (2000). Higher-Order Logic and Theorem Proving for Structured Specifications. In: Bert, D., Choppy, C., Mosses, P.D. (eds) Recent Trends in Algebraic Development Techniques. WADT 1999. Lecture Notes in Computer Science, vol 1827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-44616-3_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-44616-3_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67898-4
Online ISBN: 978-3-540-44616-3
eBook Packages: Springer Book Archive