Decompositional Proof Systems for Logics Based on Non-deterministic Matrices

                        Abstract

Non-deterministic matrices (shortly: N-matrices) are multiple-valued 
structures in which the value assigned by a valuation to a complex formula 
can be chosen non-deterministically out of a certain nonempty set of options. 
We consider two versions of semantics of a logic based on an N-matrix: 
a dynamic one and a static one.  The dynamic semantics corresponds to a fully 
non-deterministic choice of the value of any connective within the set of 
allowed options independently for each application of the connective 
(computation time choice). The static valuation, in turn, amounts to 
choosing beforehand, within the allowed set of options, one deterministic 
application of the connective  to be used in each application of the 
connective  (global choice).  For each type of semantics, we develop 
general deductive proof systems employing the R-S decomposition methodology 
for logics propositional logics based on those structures. Later we show 
how these systems can be used to obtain cut-free ordinary Gentzen calculi 
for some well-known logics.