Modeling the interaction of computing errors by four-valued contaminating logics

SZMUC, DAMIÁN ENRIQUE; CIUNI, ROBERTO; FERGUSON, THOMAS MACAULAY

Utrecht

Workshop; 26th Workshop on Logic, Language, Information and Computation; 2019

Workshop on Logic, Language, Information and Computation (WoLLIC)

Logics based on weak Kleene algebra (WKA) and related structures have been recently proposed as a tool for reasoning about flaws in computer programs. The key element of this proposal is the presence, in WKA and related structures, of a non-classical truth-value that is "contaminating" in the sense that whenever the value is assigned to a formula phi, any complex formula in which phi appears is assigned that value as well. Under such interpretations, the contaminating states represent occurrences of a flaw. However, since different programs and machines can interact with (or be nested into) one another, we need to account for different kind of errors, and this calls for an evaluation of systems with multiple contaminating values. In this paper, we make steps toward these evaluation systems by considering two logics, HYB1 and HYB2, whose semantic interpretations account for two contaminating values beside classical values 0 and 1. In particular, we provide two main formal contributions. First, we give a characterization of their relations of (mutiple-conclusion) logical consequence that is, necessary and sufficient conditions for a set Gamma of formulas to logically follow from a set Delta of formulas in HYB1 or HYB2. Second, we provide sound and complete sequent calculi for the two logics.