We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Reasoning with first order nondeterministic specifications.
- Authors
Konikowska, Beata; BiaLasik, Marcin
- Abstract
Summary. The paper presents a variant of first order logic for specifying nondeterministic software. Models of the logics are multialgebras, i.e. multi-sorted algebras with set-valued operations, together with multi-sorted valuations of variables. We allow empty carrier sets but the valuations are kept total. Terms are interpreted as sets and the usual set of algebraic terms is extended by an additional lot construct used for limiting nondeterminism. Atomic formulae are of the form t[sub 1] arrow right t[sub 2] where arrow right is a rewrite operator, corresponding semantically to inclusion. For the above logic, we develop two complete deduction systems in the natural deduction style: a Rasiowa-Sikorski system for sequences of formulae, and a cut-free Gentzen-style sequent calculus. We also consider the issues of determinism and partiality, proposing alternate solutions to defining the respective predicates in our logic.
- Subjects
FIRST-order logic; SET theory; MATHEMATICAL variables; MATHEMATICAL sequences
- Publication
Acta Informatica, 1999, Vol 36, Issue 5, p375
- ISSN
0001-5903
- Publication type
Article
- DOI
10.1007/s002360050165