Theory Structuring in Ergo 4.1

Mark Utting
Department of Computer Science, The University of Queensland, St. Lucia, QLD 4072, Australia.
marku@cs.uq.edu.au

Ray Nickson
Department of Computer Science, The University of Queensland, St. Lucia, QLD 4072, Australia.
nickson@cs.uq.edu.au

Owen Traynor
Department of Computer Science, The University of Queensland, St. Lucia, QLD 4072, Australia.
owen@cs.uq.edu.au

Abstract

For reasoning about large and complex systems, proof tools should provide sophisticated theory structuring facilities, just as programming languages should provide module facilities in order to support programming in-the-large.

This paper describes a set of theory structuring facilities that supports theory reuse effectively, provides separate name spaces and independent syntax for each theory, and fully supports interpretation and instantiation of theories. These facilities have been implemented in the Ergo 4.1 proof tool.

Conference Home Page