Generalized Program Slicing Applied to Z Specifications

Program slicing, a well-known technique, originally introduced by Weiser M., has already been widely used in numerous software engineering areas. With the development of research, the concept of program slicing is extended, and its application domains are broadened. This paper proposes a method for slicing Z formal specifications based on relations selection, relations projection and relations connection. This method does not take any time to construct dependence graphs, which decreases chance of making a mistake. Finally, it is applied to automate theorem proof, one of main artificial intelligence activities.