Meta-programming with Theory Systems

A theory system is a collection of interdependent theories, some if which stand in a meta/object relationship, forming an arbitrary number of meta-levels. The main thesis of this chapter is that theory systems constitute a suitable formalism for constructing advanced applications in reasoning and software engineering. The Alloy language for defining theory systems is introduced, its syntax is defined and a collection of inference rules is presented. A number of problems suitable for theory systems are discussed, with program examples given in Alloy. Some current implementation issues and future extensions are discussed. This paper appears as a chapter in Meta-logics and Logic Programming, edited by K. Apt and F. Turini, and published by MIT Press in 1995. 1 Outline A conventional logic program can be seen as the nonlogical axioms of a single theory. This chapter presents a thesis that we obtain a more powerful tool for applications in artificial intelligence and software engineering..