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