Quantifier-free logic for nondeterministic theories

We develop a quantifier-free logic for deriving consequences of multialgebraic theories. Multialgebras are used as models for nondeterminism in the context of algebraic specifications. They are many sorted algebras with set-valued operations. Formulae are sequents over atoms allowing one to state set-inclusion or identity of 1-element sets (determinacy). We introduce a sound and weakly complete Rasiowa-Sikorski (R-S) logic for proving multialgebraic tautologies. We then extend this system for proving consequences of specifications based on translation of finite theories into logical formulae. Finally, we show how such a translation may be avoided-introduction of the specific cut rules leads to a sound and strongly complete Gentzen system for proving directly consequences of specifications. Besides giving examples of the general techniques of R-S and the specific cut rules, we improve the earlier logics for multialgebras by providing means to handle empty carriers (as well as empty result-sets) without the use of quantifiers, and to derive consequences of theories without translation into another format and without using general cut. (c) 2006 Elsevier B.V. All rights reserved.