Logical support for modularisation (abstract)

Modularisation is important for managing the complex structures that arise in large theorem proving problems, and in large software and/or hardware development projects. This paper studies some properties of logical systems that support the definition, combination, parameterisation and reuse of modules. Our results show some new connections among: (1) the preservation of various kinds of conservative extension under pushouts; (2) various distributive laws for information hiding over sums; and (3) (Craig style) interpolation properties. In addition, we study differences between syntactic and semantic formulations of conservative extension properties, and of distributive laws. A model theoretic property that we call exactness plays an important role in some results.

This paper explores the interplay between syntax and semantics, and thus lies in the tradition of abstract model theory. We represent logical systems as institutions. An important technical foundation is a new axiomatisation of the notion of inclusion. We also show how to subsume the deduction-based approach of $\pi$-institutions under that of ordinary institutions. Our results illuminate some interesting differences between equational style logics and first order style logics, encouraging us to conclude that, on the whole, equational style logics may be more suitable for modularisation than first order style logics.
back to Selected Publications