Many-valued and Two-valued  Paradigms in Computer Science Logics

Beata Konikowska, Institute of Computer Science, Polish Academy of Sciences

The talk addresses an issue which is the subject of traditional
dispute between the proponents of two-valued, classical logic as a
universal tool for describing all phenomena examined in Computer
Science, and the supporters of many-valued logics as the most suitable
tool for that purpose. The claim put forward is that the best solution
to this dilemma is a compromise between the two opposite approaches:
the use of many-valued logics in describing the semantics of the
specific CS application we have in mind, and utilization of two-valued
proof mechanisms in reasoning about it.

The talk discusses the basic mechanisms for reducing many logical
values used in the semantics to the two classical logical values used
in reasoning about that semantics, and gives examples of the use of
the proposed hybrid approach. The concrete CS applications quoted in
those examples include a logic for reasoning about finite and infinite
program errors, a two-layered logic for program specification and
validation, a logic for combining and processing information from
various sources, and many-valued model checking of concurrent
programs.