On the Kleene Algebra of Partial Predicates with Predicate Complement Ievgen Ivanov, Mykola Nikitchenko[0000−0002−4078−1062] Taras Shevchenko National University of Kyiv, Ukraine ivanov.eugen@gmail.com, nikitchenko@unicyb.kiev.ua Abstract. In the paper we investigate the question of expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and give a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of an optimization problem. The obtained results may be useful for de- velopment of (semi-)automatic deduction tools for an extension of the Floyd-Hoare logic for the case of partial pre- and postconditions. Keywords: Formal methods, software verification, partial predicate, Floyd-Hoare logic. 1 Introduction Floyd-Hoare logic [1, 2] is a logic which is useful for proving partial correctness of sequential programs. It is based on properties of triples (assertions) of the form {p}f {q}, where f is a program and p, q are predicates which specify pre- and post-conditions. An assertion of this kind means that if the program’s input d satisfies the pre-condition p, and the program terminates on d, the program’s output satisfies the post-condition q. In the classical Floyd-Hoare logic the pro- gram is allowed to be non-terminating (or have an undefined result of execution), but the pre- and postconditions are assumed to be always defined (have a well defined truth value). In the presence of pre- and postconditions defined by par- tial predicates (which can be undefined on some data) the inference rules (in particular, the sequence rule) of the classical Floyd-Hoare logic become unsound [13, 14], when a triple {p}f {q} is understood in the following way: if a precondi- tion p is defined and true on the program’s input, and the program f terminates with a result y, and the postcondition q is defined on y, then q is true on y. In the previous works [15, 3, 4, 10, 12, 11, 8] we investigated an inference sys- tem for an extension of Floyd-Hoare logic which remains sound in the case of partial pre- and postconditions, assuming the above mentioned interpretation of Floyd-Hoare triples. The formulations of the rules of this inference system, how- ever, require introduction of a new composition into the logical language used to express pre- and postconditions. Whereas the formulation of the rules of the classical Floyd-Hoare logic depends on the usual boolean compositions (¬, ∧) of pre- and postcondition predicates (which are assumed to be total), the men- tioned extension depends on the compositions of negation (¬) and conjunction (∧) of partial predicates defined in accordance with the tables of Kleene’s strong 3-valued logic, and on one additional unary composition of partial predicates which we call the composition of predicate complement and denote as ∼. This composition extends the signature of the Kleene algebra of partial predicates [9]. In this paper we investigate the question of expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and give a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of a special constrained optimization problem. The obtained results may be useful for development of (semi-)automatic deduc- tion tools for the mentioned extension of the Floyd-Hoare logic for the case of partial pre- and postconditions. 2 Notation We will use the following notation. The notation f : A→B ˜ means that f is a partial function on a set A with values in a set B, and f : A → B means that f is a total function from A to B. For a function f : A→B: ˜ – f (x) ↓ means that f is defined on x; – f (x) ↓= y means that f is defined on x and f (x) = y; – f (x) ↑ means that f is undefined on x; – dom(f ) = {x ∈ A | f (x) ↓} is the domain of a function. We will denote as f1 (x1 ) ∼ = f2 (x2 ) the strong equality, i.e. f1 (x1 ) ↓ if and only if f2 (x2 ) ↓, and if f1 (x1 ) ↓, then f1 (x1 ) = f2 (x2 ). The symbols T, F will denote the “true” and ”false” values of predicates. We will denote Bool = {T, F }. The symbol ⊥ will denote a nowhere defined partial predicate. Let D 6= ∅ be a set, and P0 , P1 , ... Pn be partial predicates on D. Let AP rP1 ,...,Pn (D) = (D→ ˜ {T, F }; ∨, ∧, ¬, ∼, P1 , P2 , ..., Pn ) be an algebra of partial predicates with constants P1 , ..., Pn , where 1. ∨, ∧, ¬ are the operations of disjunction, conjunction and negation on partial predicates defined in accordance with Kleene’s strong three-valued logic as follows:   T, if P (d) ↓= T or Q(d) ↓= T ; (P ∨ Q)(d) = F, if P (d) ↓= F and Q(d) ↓= F ;   undefined in other cases.   T, if P (d) ↓= T and Q(d) ↓= T ; (P ∧ Q)(d) = F, if P (d) ↓= F or Q(d) ↓= F ;   undefined in other cases.   T, if P (d) ↓= F ; (¬P )(d) = F, if P (d) ↓= T ;   undefined in other case. 2. ∼ is the unary operation of predicate complement: ( T, if P (d) ↑; (∼ P )(d) = undefined, if P (d) ↓ . We will call AP rP1 ,...,Pn (D) the Kleene algebra of partial predicates on D with predicate complement and constants P1 , ..., Pn . 3 Main Result Let F (n) be the set of all n-ary functions (operations) f : {−1, 0, 1}n → {−1, 0, 1}. The elements of F (n) will represent functions of 3-valued logic P3 (where 1 cor- responds to the “true” value and −1 corresponds to the “false” value, and 0 is an intermediate S truth value). Let F = n≥0 F (n) . We will denote as x ˉ = (x1 , x2 , ..., xn ) a tuple of values xi ∈ {−1, 0, 1}. Let us consider {−1, 0, 1}n as a metric space with Chebyshev distance: n ρn ((x1 , ..., xn ), (y1 , ..., yn )) = max |xi − yi |. i=1 We will say that a function f ∈ F (n) is short, if it is a short map, i.e. if for all x ˉ, yˉ we have |f (ˉ x) − f (ˉ y )| ≤ ρn (ˉ x, yˉ). For any predicate P : D→{T, ˜ F } denote by Φ(P ) a function D → {−1, 0, 1} such that for all d ∈ D:   1, if P (d) ↓= T, Φ(P )(d) = 0, if P (d) ↑,   −1, if P (d) ↓= F. Let D 6= ∅ be a set, P1 , P2 , ..., Pn : D→{T, ˜ F } be partial predicates, and AP rP1 ,...,Pn (D) = (D→ ˜ {T, F }; ∨, ∧, ¬, ∼, P1 , P2 , ..., Pn ). Let pi = Φ(Pi ) for P i = 0, 1, 2, ..., n. Denote ||f || = xˉ∈{−1,0,1}n |f (ˉ x)| for f ∈ F (n) and consider the following (constrained) optimization problem1 : ||f || → min (1) f (p1 (d), p2 (d), ..., pn (d)) = p0 (d), d ∈ D (2) Theorem 1. If n ≥ 1, a predicate P0 is expressible in the algebra AP rP1 ,...,Pn (D) if and only if on the set F (n) the problem (1)-(2) has an optimal solution which is a short function. 1 If one interprets partiality in terms as possibility, minimization of ||f || may be related to the principle of minimum specificity of D. Dubois et al. from possibility theory, or other similar principles. 4 Proof of the Main Result Denote for all x, y ∈ {−1, 0, 1}: ¬x = −x ∼ x = 1 − |x|   x, if y = 1 [y] x = ∼ x, if y = 0   ¬x, if y = −1 [y ] x, yˉ) = 1 − minni=1 xi i for every n ≥ 1 and x Lemma 1. ρn (ˉ ˉ, yˉ ∈ {−1, 0, 1}n . Proof. It is easy to see that for all x, y ∈ {−1, 0, 1}: x[y] = 1 − |x − y| [y ] [y ] x, yˉ) = maxni=1 |xi − yi | = maxni=1 (1 − xi i ) = 1 − minni=1 xi i . Then ρn (ˉ t u Consider {−1, 0, 1} as a lattice with operations: x ∨ y = max(x, y); x ∧ y = min(x, y). Below we will assume that in expressions involving operations on {−1, 0, 1} the operation x[y] has the highest priority, and is followed (by priority) by the unary operations ¬, ∼, which are followed by the binary operations ∧ and ∨. As usual, among ∧, ∨, the operation ∧ has higher priority. Lemma 2. For each short function f ∈ F (n) and x ˉ ∈ {−1, 0, 1}n : x) = fˆ(ˉ f (ˉ x) ∨ ¬f6=0 (ˉ x) ∧ f6=0 (ˉ x) where (W Vn [yi ] i=1 xi , if ∃ˉ y f (ˉ y) = 1 fˆ(ˉ x) = yˉ:f (ˉ y )=1 −1, otherwise (W Vn [yi ] [yi ] [yi ] yˉ:f (ˉ y )6=0 i=1 ∼ (xi ∧ ∼ xi )∧ ∼∼ xi , if ∃ˉ y ) 6= 0 y f (ˉ f6=0 (ˉ x) = . 0, otherwise. Proof. It is easy to see that for each x, y ∈ {−1, 0, 1}: ( [y] [y] [y] 1, if x = y ∼ (x ∧ ∼ x )∧ ∼∼ x = 0, if x 6= y. Then ( 1, x) 6= 0 if f (ˉ f6=0 (ˉ x) = 0, if f (ˉ x) = 0. By Lemma 1, (W y )=1 (1 − ρn (ˉ x, yˉ)), if ∃ˉ y f (ˉ y ) = 1, fˆ(ˉ x) = yˉ:f (ˉ −1, otherwise. x) = 1, then fˆ(ˉ If f (ˉ x) = 1 and f6=0 (ˉ x) = 1, so fˆ(ˉ x) ∧ f6=0 (ˉ x) ∨ ¬f6=0 (ˉ x) = 1. x) = 0, then f6=0 (ˉ If f (ˉ x) = 0, so fˆ(ˉ x) ∧ f6=0 (ˉ x) = (fˆ(ˉ x) ∨ ¬f6=0 (ˉ x) ∧ 0) ∨ 0 = 0. x) = −1, then for each yˉ such that f (ˉ If f (ˉ y ) = 1 we have ρn (ˉ x, yˉ) ≥ |f (ˉ x) − y )| = 2 which implies that 1−ρn (ˉ f (ˉ x, yˉ) = −1. Then fˆ(ˉ x) = −1 and f6=0 (ˉ x) = 1, so fˆ(ˉx) ∧ f6=0 (ˉ x) ∨ ¬f6=0 (ˉ x) = −1. Thus x) = fˆ(ˉ f (ˉ x) ∨ ¬f6=0 (ˉ x) ∧ f6=0 (ˉ x). t u Lemma 3. The set of all short functions from F is a precomplete class in F and is the functional closure of the set {f0 , f1 , f2 , f3 , f4 }, where f0 ∈ F (0) , f1 , f2 ∈ F (1) , f3 , f4 ∈ F (2) and f0 = 0, f1 (x) = −x, f2 (x) = 1−|x|, f3 (x, y) = max(x, y), f4 (x, y) = min(x, y). Proof. Denote by S the set of all short functions from F . In accordance with its definition, a short function from F can be alternatively characterized as a n function {−1, Qn0, 1} → {−1, 0, 1} (n ≥ 0) which does not change sign on each of the sets i=1 {0, ai }, where a1 , ..., an ∈ {−1, 1}n . In the terminology of [18], such functions correspond to the precomplete class TE31 ,1 of functions for which the image of the product of sets, 1-equivalent to E1 is a subset of a set, 1- equivalent to E1 , where two sets are 1-equivalent, if their symmetric difference has no more than 1 element. Thus S is a precomplete class in F . Obviously, {f0 , f1 , f2 , f3 , f4 } ⊆ S. On the other hand, since the constant function with value −1 is expressible as f1 ◦ f2 ◦ f0 , from Lemma 2 and the definition of x[y] it follows that each f ∈ S can be expressed as a composition of elements of {f0 , f1 , f2 , f3 , f4 } and of projections πkn (x1 , ..., xn ) = xk (n ≥ 1, k = 1, 2, ..., n). Thus S is the functional closure of {f0 , f1 , f2 , f3 , f4 }. t u Lemma 4. For each P, Q : D→{T,˜ F } and d ∈ D we have: Φ(⊥)(d) = 0 Φ(¬P )(d) = −(Φ(P )(d)) Φ(∼ P )(d) = 1 − |Φ(P )(d)| Φ(P ∨ Q)(d) = max(Φ(P )(d), Φ(Q)(d)) Φ(P ∧ Q)(d) = min(Φ(P )(d), Φ(Q)(d)) Proof. Follows immediately from the definition Φ and operations ¬, ∼, ∨, ∧ on partial predicates. t u Let M (n) be the set of all short functions from F (n) . Lemma 5. The problem (1)-(2) has an optimal solution on F (n) if and only if p0 is continuous in the initial topology on D induced by p1 , ..., pn (where the codomain of pi , {−1, 0, 1}, is considered as a discrete space). Proof. “If”: assume that p0 is continuous in the initial topology on D induced by p1 , ..., pn . Then there exists f ∈ F (n) such that p0 (d) = f (p1 (d), ..., pn (d)) for all d ∈ D. Then since the set F (n) is finite, the problem (1)-(2) has an optimal solution on F (n) . “Only if”: assume that the problem (1)-(2) has an optimal solution f ∈ F (n) . Then p0 (d) = f (p1 (d), ..., pn (d)) for all d ∈ D, so p0 is continuous in the initial topology on D induced by p1 , ..., pn . t u Lemma 6. If the problem (1)-(2) has an optimal solution on F (n) , then this solution is unique. Proof. Assume that the problem (1)-(2) has optimal solutions f, g ∈ F (n) . Then ||f || = ||g|| and f (p1 (d), ..., pn (d)) = p0 (d) = g(p1 (d), ..., pn (d)) for all d ∈ D. Suppose that f 6= g. Then there exists x ˉ∗ = (x∗1 , ..., x∗n ) ∈ {−1, 0, 1}n such ∗ ∗ that f (ˉ x ) 6= g(ˉx ). Consider the case when f (ˉ x∗ ) 6= 0. Let us define a function h ∈ F (n) as ∗ follows: h(ˉ x) = f (ˉ ˉ 6= x x), if x ˉ , and h(ˉ x) = 0, if x ˉ=x ˉ∗ . Then for all d ∈ D, ∗ (p1 (d), ..., pn (d)) 6= xˉ , so h(p1 (d), ..., pn (d)) = p0 (d). Moreover, ||h|| = ||f || − x∗ )| = ||f || − 1 < ||f || which contradicts the assumption that f is an optimal |f (ˉ solution of (1)-(2). Consider the case when f (ˉ x∗ ) = 0. Then |g(ˉ x∗ )| = 1. Let us define a function ∗ h ∈ F (n) as follows: h(ˉ x) = g(ˉ ˉ 6= x x), if x ˉ , and h(ˉ x) = 0, if xˉ = x ˉ∗ . Then ∗ for all d ∈ D, (p1 (d), ..., pn (d)) 6= x ˉ , so h(p1 (d), ..., pn (d)) = p0 (d). Moreover, ||h|| = ||g|| − |g(ˉ x∗ )| = ||g|| − 1 < ||g|| which contradicts the assumption that g is an optimal solution of (1)-(2). Thus f = g. So if the problem (1)-(2) has an optimal solution on F (n) , then this solution is unique. t u Lemma 7. Let f ∈ M (n) , g ∈ F (n) and g(ˉ x) ∈ {f (ˉ ˉ ∈ {−1, 0, 1}n . x), 0} for each x (n) Then g ∈ M . Proof. Let x ˉ, yˉ ∈ {−1, 0, 1}n . Consider the following cases. 1) g(ˉ x) = f (ˉ x), g(ˉ y ) = f (ˉ y ). Then |g(ˉ x) − g(ˉ y )| = |f (ˉ x) − f (ˉ y )| ≤ ρ(ˉx, yˉ). 2) g(ˉ x) = f (ˉ y ) = 0. Then |g(ˉ x), g(ˉ x) − g(ˉy )| = |f (ˉ x)| ≤ ρ(ˉ ˉ 6= yˉ, and x, yˉ), if x |g(ˉ x) − g(ˉy )| = 0 ≤ ρ(ˉ x, yˉ), if xˉ = yˉ. 3) g(ˉ x) = 0, g(ˉ y ) = f (ˉy ). Then |g(ˉ x) − g(ˉy )| = |f (ˉ y )| ≤ ρ(ˉ ˉ 6= yˉ, and x, yˉ), if x |g(ˉ x) − g(ˉy )| = 0 ≤ ρ(ˉ x, yˉ), if xˉ = yˉ. 4) g(ˉ x) = 0, g(ˉ y ) = 0. Then |g(ˉ x) − g(ˉ y )| ≤ ρ(ˉ x, yˉ). Thus g ∈ M (n) . t u Lemma 8. The problem (1)-(2) has an optimal solution on M (n) if and only if it has an optimal solution on F (n) which belongs to M (n) . Proof. “If”: assume that the problem (1)-(2) has an optimal solution f ∈ F (n) which belongs to M (n) . Then f (p1 (d), p2 (d), ..., pn (d)) = p0 (d) for all d ∈ D. Moreover, for each g ∈ M (n) such that g(p1 (d), p2 (d), ..., pn (d)) = p0 (d) for all d ∈ D, we have g ∈ F (n) , so ||f || ≤ ||g||. So f is an optimal solution of (1)-(2)on M (n) . “Only if”: assume that the problem (1)-(2) has an optimal solution f on M (n) . Then f (p1 (d), p2 (d), ..., pn (d)) = p0 (d) for all d ∈ D. Then since F (n) is finite, the problem (1)-(2) has an optimal solution on F (n) . By Lemma 6, the problem (1)-(2) has a unique optimal solution of F (n) . Denote it as g. Then g(p1 (d), p2 (d), ..., pn (d)) = p0 (d) for all d ∈ D and ||g|| ≤ ||f ||. Let us define a function h ∈ F (n) as follows: for each x ˉ ∈ {−1, 0, 1}n , h(ˉ x) = f (ˉ x) 6= 0, x), if g(ˉ and h(ˉ x) = g(ˉ x), if g(ˉ x) = 0. Then for all d ∈ D, h(p1 (d), ..., pn (d)) = p0 (d). Moreover, h ∈ M (n) by Lemma 7. Then ||h|| = ||f ||, so for each x ˉ such that g(ˉx) = 0 we have f (ˉ x) = 0. Then ||f || ≤ ||g||. Since ||g|| ≤ ||f || as mentioned above, we have ||f || = ||g||. The f is an optimal solution of (1)-(2) on F (n) and f belongs to M (n) . t u Now we can give a proof of the main Theorem 1 from the previous section. Proof (of Theorem 1). “If”: assume that the problem (1)-(2) has an optimal solution on the set F (n) which is a short function. Denote by f such a solution. Then we have p0 (d) = f (p1 (d), p2 (d), ..., pn (d)) for all d ∈ D. By Lemma 3, f belongs to the functional closure of {f0 , f1 , f2 , f3 , f4 }, where fi are defined as in Lemma 3. From Lemma 4 it follows that p0 (d) = Φ(P )(d) for all d ∈ D for some predicate P : D→{T, ˜ F } expressible in the algebra (D→ ˜ {T, F }; ∨, ∧, ¬, ∼ , ⊥, P1 , P2 , ..., Pn ). Since n ≥ 1 and the predicate ⊥ can be expressed as ∼ P1 ∧ ∼∼ P1 , we conclude that P is expressible in the algebra AP rP1 ,...,Pn (D). Then Φ(P0 )(d) = Φ(P )(d) for all d ∈ D. Then the definition of Φ implies that P0 = P , so P0 is expressible in AP rP1 ,...,Pn (D). “Only if”: assume that a predicate P0 is expressible in algebra AP rP1 ,...,Pn (D). Then Lemma 4 implies that Φ(P0 )(d) = f (Φ(P1 )(d), Φ(P2 )(d), ..., Φ(Pn )(d)) for all d ∈ D for some function f ∈ F (n) which belongs to the functional closure of {f0 , f1 , f2 , f3 , f4 }, where fi are defined as in Lemma 3. Then by Lemma 3, f is a short function and p0 (d) = f (p1 (d), ..., pn (d)) for all d ∈ D. Then since M (n) ⊆ F (n) is a finite set, the problem (1)-(2) has an optimal solution on the set M (n) . Then Lemma 8 implies that the problem (1)-(2) has an optimal solu- tion on F (n) which is a short function. t u Note that the problem (1)-(2) has the following addition property. Lemma 9. If the problem (1)-(2) has an optimal solution on M (n) , then this solution is unique. Proof. Assume that f, g are optimal solutions of (1)-(2) on M (n) . Then by Lemma 8, (1)-(2) has an optimal solution on F (n) which belongs to M (n) . By Lemma 6 this solution is unique. Denote it as h. Then ||h|| ≤ ||f || and ||h|| ≤ ||g||. Then h is an optimal solution of (1)-(2) on M (n) and ||h|| = ||f || = ||g||. Then f , g are optimal solutions of (1)-(2) on F (n) . Then by Lemma 6, f = g. t u 5 Example In this example of application of the main result of the paper we will use the notation and terminology of the composition-nominative approach to program formalization [16, 17] and [7, 6, 5]. Let v be a fixed name, V = {v}, A = {T, F }. Let D = V A be the set of named sets on V which take values in A. Then D = {[], [v 7→ T ], [v 7→ F ]}. Let P1 be a partial predicate on D such that P1 (d) ∼ = (v ⇒ (d)) where v ⇒ is the denaming operation [16, 17] (which has undefined value, if v∈ / dom(d)). Let P0 be a partial predicate on D such that ( T, if v ⇒ (d) ↑; P0 (d) = F, if v ⇒ (d) ↓ . Let us check if P0 is expressible in the algebra AP rP1 (D) = (D→{T, ˜ F }; ∨, ∧, ¬, ∼, P1 ).  → {−1, 0, 1}, i = 0, 1 be functions such that Let pi : D  1, if Pi (d) ↓= T, pi (d) = 0, if Pi (d) ↑,   −1, if Pi (d) ↓= F. Then   1, if v ⇒ (d) ↓= T, p1 (d) = 0, if v ⇒ (d) ↑,   −1, if v ⇒ (d) ↓= F.   −1, if v ⇒ (d) ↓= T, p0 (d) = 1, if v ⇒ (d) ↑,   −1, if v ⇒ (d) ↓= F. The initial topology on D induced by p1 is the power set of D, so p0 is continuous. We have p0 ({d ∈ D | p1 (d) = −1}) = {−1} p0 ({d ∈ D | p1 (d) = 0}) = {1} p0 ({d ∈ D | p1 (d) = 1}) = {−1} Then a function with the graph {(−1, −1), (0, 1), (1, −1)} is the unique optimal solution of the problem (1)-(2), but it is, obviously, not a short function. Then Theorem 1 implies that P0 is not expressible in the algebra AP rP1 (D) = (D→{T, ˜ F }; ∨, ∧, ¬, ∼, P1 ). 6 Conclusion We have investigated the question of expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and have given a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of a special optimization problem. The obtained results may be useful for development of (semi-)automatic deduction tools for an extension of the Floyd-Hoare logic for the case of partial pre- and postconditions. References 1. Floyd, R.: Assigning meanings to programs. Mathematical aspects of computer science 19(19-32) (1967) 2. Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) 3. Ivanov, I., Kornilowicz, A., Nikitchenko, M.: Implementation of the composition- nominative approach to program formalization in mizar. Computer Science Journal of Moldova 26, 59–76 4. Ivanov, I., Kornilowicz, A., Nikitchenko, M.: Formalization of nominative data in mizar. pp. 82–85. Proceedings of TAAPSD 2015, 23-26 December 2015, Taras Shevchenko National University of Kyiv, Ukraine (2015) 5. Ivanov, I.: An abstract block formalism for engineering systems. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G., Zavileysky, M., Kravtsov, H., Kobets, V., Peschanenko, V.S. (eds.) Proceedings of the 9th In- ternational Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Kherson, Ukraine, June 19- 22, 2013. CEUR Workshop Proceedings, vol. 1000, pp. 448–463. CEUR-WS.org (2013) 6. Ivanov, I.: On existence of total input-output pairs of abstract time systems. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) Information and Communication Technologies in Education, Research, and Industrial Applications. Communications in Computer and Information Science, vol. 412, pp. 308–331. Springer International Publishing, Cham (2013) 7. Ivanov, I.: On representations of abstract systems with partial inputs and outputs. In: Gopal, T.V., Agrawal, M., Li, A., Cooper, S.B. (eds.) Theory and Applications of Models of Computation. Lecture Notes in Computer Science, vol. 8402, pp. 104–123. Springer International Publishing, Cham (2014) 8. Ivanov, I., Nikitchenko, M.: Inference rules for the partial floyd-hoare logic based on composition of predicate complement. In: Ermolayev, V., Suárez-Figueroa, M.C., Yakovyna, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A. (eds.) Information and Communication Technologies in Education, Research, and Industrial Applications. pp. 71–88. Springer International Publishing, Cham (2019) 9. Kornilowicz, A., Ivanov, I., Nikitchenko, M.: Kleene algebra of partial predicates. Formalized Mathematics 26, 11–20 (2018) 10. Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to for- malization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th Inter- national Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15-18, 2017. pp. 504–523 (2017) 11. Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems. ACSIS, vol. 11, pp. 237–244 (2017) 12. Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the Nominative Algorithmic Algebra in Mizar, Advances in Intelligent Systems and Computing, vol. 656, pp. 176–186. Springer International Publishing, Cham (2018) 13. Kryvolap, A., Nikitchenko, M., Schreiner, W.: Extending Floyd-Hoare logic for partial pre- and postconditions. In: Ermolayev, V., Mayr, H., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) Information and Communication Tech- nologies in Education, Research, and Industrial Applications, Communications in Computer and Information Science, vol. 412, pp. 355–378. Springer International Publishing (2013) 14. Nikitchenko, M., Kryvolap, A.: Properties of inference systems for Floyd-Hoare logic with partial predicates. Acta Electrotechnica et Informatica 13(4), 70–78 (2013) 15. Nikitchenko, M., Ivanov, I., Kornilowicz, A., Kryvolap, A.: Extended Floyd-Hoare logic over relational nominative data. In: Bassiliades, N., Ermolayev, V., Fill, H.G., Yakovyna, V., Mayr, H.C., Nikitchenko, M., Zholtkevych, G., Spivakovsky, A. (eds.) Information and Communication Technologies in Education, Research, and Industrial Applications. pp. 41–64. Springer International Publishing, Cham (2018) 16. Nikitchenko, N.S.: A composition nominative approach to program semantics. Tech. rep., IT-TR 1998-020, Technical University of Denmark (1998) 17. Skobelev, V., Nikitchenko, M., Ivanov, I.: On algebraic properties of nominative data and functions. In: Ermolayev, V., Mayr, H., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) Information and Communication Technologies in Education, Research, and Industrial Applications, Communications in Computer and Infor- mation Science, vol. 469, pp. 117–138. Springer International Publishing (2014) 18. Yablonskii, S.: Functional constructions in a k-valued logic. Trudy Mat. Inst. Steklov. 51, 5–142 (1958)