Non-deterministic 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 different types of semantics which are based on Nmatrices: the dynamic one and the static one . We use the Rasiowa-Sikorski decomposition methodology to get sound and complete proof systems employing finite sets of mv-signed formulas for all propositional logics based on such structures with either of the above (...) types of semantics. Later we demonstrate how these systems can be converted into cut-free ordinary Gentzen calculi which are also sound and complete for the corresponding non-deterministic semantics. As a by-product, we get new semantic characterizations for some well-known logics. (shrink)

. The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have designated values or not. The transformation preserves the general (...) structure of proofs in the original calculus in a way ensuring preservation of the weak cut elimination theorem under the transformation. The described transformation metod is illustrated on several concrete examples of many-valued logics, including a new application to information sources logics. (shrink)

A similarity relation is a reflexive and symmetric binary relation between objects. Similarity is relative: it depends on the set of properties of objects used in determining their similarity or dissimilarity. A multi-modal logical language for reasoning about relative similarities is presented. The modalities correspond semantically to the upper and lower approximations of a set of objects by similarity relations corresponding to all subsets of a given set of properties of objects. A complete deduction system for the language is presented.

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a (...) non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. (shrink)

The main goal of the paper is to suggest some analytic proof systems for LC and its finite-valued counterparts which are suitable for proof-search. This goal is achieved through following the general Rasiowa-Sikorski methodology for constructing analytic proof systems for semantically-defined logics. All the systems presented here are terminating, contraction-free, and based on invertible rules, which have a local character and at most two premises.

A formal language of two-valued logic is developed, whose terms are formulas of the language of Kleene's three-valued logic. The atomic formulas of the former language are pairs of formulas of the latter language joined by consequence operators. These operators correspond to the three sensible types of consequence (strong-strong, strong-weak and weak-weak) in Kleene's logic in analogous way as the implication connective in the classical logic corresponds to the classical consequence relation. The composed formulas of the considered language are built (...) from the atomic ones by means of the classical connectives and quantifiers.A deduction system for the developed language is given, consisting of a set of decomposition rules for sequences of formulas. It is shown that the deduction system is sound and complete. (shrink)

ABSTRACT Two objects o1, o2 of an information system are said to be complementary with respect to attribute a if α(o1) = -α(o2), where α(o) is the set of values of attribute a assigned to o. They are said to be complementary with respect to a set of attributes A if they are complementary with respect to each attribute α ε A. A multi-modal logical language for reasoning about complementarity relations is presented, with modalities [A] and ?A? parameterised by subsets (...) of a given set ATTR of attributes. Two complete deduction system for the language are presented: a Rasiowa-Sikorski style system using signed formulae, and an equivalent sequent calculus system in Gentzen style complete for theories. (shrink)

The paper discusses a four-valued propositional logic FOUR≤, similar to Belnap's logic, which can be used to describe incomplete or inconsistent knowledge. In addition to the two classical logical values tt, ff, FOUR≤ features also two nonclassical values: ⊥, representing incomplete information, and ⊤, representing inconsistency. The nonclassical values are incomparable, and together with the classical ones they form a diamond-shaped lattice L4 known from Belnap's logic, which underlies the semantics of FOUR≤. The set of connectives contains those of Belnap's (...) logic, together with an additional operator representing the lattice order, which decisively increases the expressive power of the logic. In the paper we develop a complete decompositional deduction system in Rasiowa-Sikorski style for FOUR≤. (shrink)