Generated models and the ω-rule: The nondeterministic case

A language for specifying nondeterministic operations which generalizes the equational specification language is introduced. Then, various notions of generated multimodels are discussed and sufficient conditions for the existence of quasi-initial semantics of nondeterministic specifications are given. Two calculi are introduced: NEQ and NIP. The former is sound and complete with respect to the class of all multimodels. The latter is an extension of the former with the ω-rule. It is sound and complete with respect to one of the classes of the generated multimodels. The calculi reduce to the respective deterministic calculi whenever the specification involves only deterministic operations.