Beata Konikowska

Rasiowa-Sikorski Deduction Systems in Computer Science Applications

916

Abstract

The aim of the paper is to advertise a methodology of developing deduction systems for various logics 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-valued temporal logic for concurrency.

Key words: deduction systems, computer science logics, many-valued logics, many-sorted logics, modal logics, temporal logics.