Marcin Bialasik, Beata Konikowska

Reasoning with First Order Nondeterministic Specifications

830

Abstract

The paper presents a variant of first order logic for specifying nondeterministic software constructions. Models of the logics are multialgebras: multi-sorted algebras with set-valued operations, together with multi-sorted valuations of variables. An important issue is that empty carriers of some sorts are allowed - however, the valuations are kept total by assigning the empty set as the value of any variable of sort s if the carrier of sort s is empty. Terms of the language are interpreted as sets; an additional term-forming operator is the {\sf let} construct used for limiting nondeterminism. Atomic formulae of the logic are constructed by joining pairs of terms with a rewrite operator, corresponding semantically to inclusion of respective sets.

For the above logic, we develop two complete deduction systems in the natural deduction style: first a Rasiowa-Sikorski system for decomposing sequences of formulae, and out of it -- a Gentzen-style sequent calculus. We also consider the issues of determinism and partiality, proposing some alternate solutions for defining the respective predicates within our logic.