Wyniki wyszukiwania - BazTech

1

Finite-valued Logics for Information Processing

Avron A., Konikowska B.

Fundamenta Informaticae

|

2012

|

Vol. 114, nr 1

1-30

EN

We examine the issue of collecting and processing information from various sources, which involves handling incomplete and inconsistent information. Inspired by the framework first proposed by Belnap, we consider structures consisting of information sources which provide information about the values of formulas of classical propositional logic, and a processor which collects that information and extends it by deriving conclusions following from it according to the truth tables of classical logic, applied forward and backward. Our model extends Belnap’s in allowing the sources to provide information also about complex formulas. As that framework cannot be captured using finite ordinary logical matrices, if we want to represent each of the relevant logics with a single matrix, we employ Nmatrices for that purpose. In opposition to the approach proposed in our earlier work, we assume that the information sources are reasonable, i.e. that they provide information consistent with certain coherence rules. We provide sound and complete sequent calculi admitting strong cut elimination for the logic of a single information source, and (several variants of) the logic generated by the source and processor structures described above. In doing this, we also provide new characterizations for some known logics. We prove that, in opposition to the variantwith unconstrained information sources considered earlier, the latter logic cannot be generated by structures with any bounded number of sources.

2

A Multi-modal Logic for Disagreement and Exhaustiveness

Düntsch I., Konikowska B.

Fundamenta Informaticae

|

2007

|

Vol. 75, nr 1-4

215-238

EN

The paper explores two basic types of relations betwen objects of a Pawlak-style information system generated by the values of some attribute of those objects: disagreement (disjoint sets of values) and exhaustiveness (sets of values adding up to the whole universe of the attribute). Out of these two fundamental types of relations, most other types of relations on objects of an information system considered in the literature can be derived - as, for example, indiscernibility, similarity and complementarity. The algebraic properties of disagreement and indiscernibility relations are explored, and a representation theorem for each of these two types of relations is proved. The notions of disagreement and exhaustiveness relations for a single attribute are extended to relations generated by arbitrary sets of attributes, yielding two families of relations parametrized by sets of attributes. They are used as accessibility relations to define a multi-modal logic with modalities corresponding to the lower and upper approximation of a set in Pawlak's rough set theory. Finally, a complete Rasiowa-Sikorski deduction system for that logic is developed.

3

Proof Systems for Logics Based on Non-deterministic Multiple-valued Structures

Avron A., Konikowska B.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2004

|

Nr 976

1-26

EN

Non-deterministic matrices (Nmatrices) 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 (the latter is new here). We use the Rasiowa-Sikorski (R-S) 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 (like the logic CAR from [18, 28]).

PL

Macierze niedeterministyczne to wielowartościowe struktury, w których wartość przypisaną przez wartościowanie złożonej formule można wybrać w niedeterministyczny sposób z pewnego niepustego zbioru opcji. Opracowujemy ogólne dedukcyjne systemy dowodzenia dla logik opartych na tych strukturach z użyciem mechanizmu n-sekwentów oraz dekompozycyjnej metodologii R-S. Później pokazujemy, jak można użyć tych systemów do uzyskania zwykłych rachunków Gentzenowskich bez reguły cięcia dla pewnych dobrze znanych logik tolerujących sprzeczność.

4

On Designated Values in Multi-Valued CTLS* Model Checking

Konikowska B., Penczek W.

Fundamenta Informaticae

|

2004

|

Vol. 60, nr 1-4

211--224

EN

A multi-valued version of CTLS* (mv-CTLS*), where both the propositions and the accessibility relation are multi-valued, taking values in a complete lattice with a complement, is considered. Contrary to all the existing model checking results for multi-valued modal logics, our lattices are not required to be finite. A set of restrictions is provided under which there is a direct translation from mv-CTLS* to CTLS* model checking problem for designated values. Bisimulation induced by mv-CTLS* is characterized.

5

Rasiowa-Sikorski deduction system in computer science applications

Konikowska B.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2000

|

nr 916

1-30

EN

The aim of the paper is to advertise a methodology of developing deduction systems for various logic based on the analysis of their semantics. This is achieved by "mirroring" the semantics of all the logical constructs (connectives, quantifiers, modalities, …) through invertible rules operating on sequences of formulae of the logic. The methodology is based on the use of a simple and universal deduction formalism developed by the Polish logicians H. Rasiowa and R. Sikorski. The paper presents a general outline of this methodology, and shows examples of its applications to various brands of computer science logics coming from the author's works, including many-valued logics, nondeterminism, similarity, indiscerniblity and complementarity, many-sorted FOL, and a new three-valeud temporal logic for concurrency.

PL

Celem pracy jest rozpropagowanie metodologii opracowywania systemów dedukcyjnych dla różnych logik na bazie ich semantyki. Osiąga się to przez odzwierciedlanie semantyki wszystkich konstruktorów logicznych (spójników, kwantyfikatorów, modalności, ...) za pomocą odwracalnych reguł działających na ciągach formuł. Metodologia ta oparta jest na zastosowaniu prostego i uniwersalnego mechanizmu dedukcyjnego opracowanego przez polskich logików: H. Rasiową i R. Sikorskiego. W pracy przedstawia się ogólny zarys tej metodologii i ukazuje przykłady jej zastosowania do wielu różnych rodzajów logik informatycznych pochodzące z prac autorki, obejmujące logiki wielowartościowe, niedeterminizm, podobieństwo, nieodróżnialność i komplementarność, wielorodzajową logikę I rzędu oraz nową trójwartościową logikę dla współbieżności.