Algebras and logics of partial quasiary predicates
In the paper we investigate algebras and logics defined for classes of partial quasiary predicates. Informally speaking, such predicates are partial predicates defined over partial states (partial assignments) of variables. Conventional n-ary predicates can be considered as a special case of quasiar...
Gespeichert in:
| Veröffentlicht in: | Algebra and Discrete Mathematics |
|---|---|
| Datum: | 2017 |
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | English |
| Veröffentlicht: |
Інститут прикладної математики і механіки НАН України
2017
|
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/156020 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Algebras and logics of partial quasiary predicates / M. Nikitchenko, S. Shkilniak // Algebra and Discrete Mathematics. — 2017. — Vol. 23, № 2. — С. 263–278. — Бібліогр.: 7 назв. — англ. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-156020 |
|---|---|
| record_format |
dspace |
| spelling |
Nikitchenko, M. Shkilniak, S. 2019-06-17T18:55:28Z 2019-06-17T18:55:28Z 2017 Algebras and logics of partial quasiary predicates / M. Nikitchenko, S. Shkilniak // Algebra and Discrete Mathematics. — 2017. — Vol. 23, № 2. — С. 263–278. — Бібліогр.: 7 назв. — англ. 1726-3255 2010 MSC:03G25, 08A70, 03B70. https://nasplib.isofts.kiev.ua/handle/123456789/156020 In the paper we investigate algebras and logics defined for classes of partial quasiary predicates. Informally speaking, such predicates are partial predicates defined over partial states (partial assignments) of variables. Conventional n-ary predicates can be considered as a special case of quasiary predicates. The notion of quasiary predicate, as well as the notion of quasiary function, is used in computer science to represent semantics of computer programs and their components. We define extended first-order algebras of partial quasiary predicates and investigate their properties. Based on such algebras we define a logic with irrefutability consequence relation. A sequent calculus is constructed for this logic, its soundness and completeness are proved. This work was supported in part by the project “Development of logic-algorithmic methods for investigation of formal models of natural languages” of Taras Shevchenko National University of Kyiv, Ukraine, Ref. Nr. 0116U004780. en Інститут прикладної математики і механіки НАН України Algebra and Discrete Mathematics Algebras and logics of partial quasiary predicates Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Algebras and logics of partial quasiary predicates |
| spellingShingle |
Algebras and logics of partial quasiary predicates Nikitchenko, M. Shkilniak, S. |
| title_short |
Algebras and logics of partial quasiary predicates |
| title_full |
Algebras and logics of partial quasiary predicates |
| title_fullStr |
Algebras and logics of partial quasiary predicates |
| title_full_unstemmed |
Algebras and logics of partial quasiary predicates |
| title_sort |
algebras and logics of partial quasiary predicates |
| author |
Nikitchenko, M. Shkilniak, S. |
| author_facet |
Nikitchenko, M. Shkilniak, S. |
| publishDate |
2017 |
| language |
English |
| container_title |
Algebra and Discrete Mathematics |
| publisher |
Інститут прикладної математики і механіки НАН України |
| format |
Article |
| description |
In the paper we investigate algebras and logics defined for classes of partial quasiary predicates. Informally speaking, such predicates are partial predicates defined over partial states (partial assignments) of variables. Conventional n-ary predicates can be considered as a special case of quasiary predicates. The notion of quasiary predicate, as well as the notion of quasiary function, is used in computer science to represent semantics of computer programs and their components. We define extended first-order algebras of partial quasiary predicates and investigate their properties. Based on such algebras we define a logic with irrefutability consequence relation. A sequent calculus is constructed for this logic, its soundness and completeness are proved.
|
| issn |
1726-3255 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/156020 |
| citation_txt |
Algebras and logics of partial quasiary predicates / M. Nikitchenko, S. Shkilniak // Algebra and Discrete Mathematics. — 2017. — Vol. 23, № 2. — С. 263–278. — Бібліогр.: 7 назв. — англ. |
| work_keys_str_mv |
AT nikitchenkom algebrasandlogicsofpartialquasiarypredicates AT shkilniaks algebrasandlogicsofpartialquasiarypredicates |
| first_indexed |
2025-11-25T22:12:50Z |
| last_indexed |
2025-11-25T22:12:50Z |
| _version_ |
1850560833796440064 |
| fulltext |
Algebra and Discrete Mathematics RESEARCH ARTICLE
Volume 23 (2017). Number 2, pp. 263–278
c© Journal “Algebra and Discrete Mathematics”
Algebras and logics
of partial quasiary predicates∗
Mykola Nikitchenko and Stepan Skilniak
Communicated by A. P. Petravchuk
Abstract. In the paper we investigate algebras and logics
defined for classes of partial quasiary predicates. Informally speaking,
such predicates are partial predicates defined over partial states
(partial assignments) of variables. Conventional n-ary predicates can
be considered as a special case of quasiary predicates. The notion of
quasiary predicate, as well as the notion of quasiary function, is used
in computer science to represent semantics of computer programs
and their components. We define extended first-order algebras of
partial quasiary predicates and investigate their properties. Based
on such algebras we define a logic with irrefutability consequence
relation. A sequent calculus is constructed for this logic, its soundness
and completeness are proved.
Introduction
Logics of quasiary predicates can be considered as a natural generali-
zation of classical predicate logic. The latter is based upon total n-ary
predicates which represent fixed and static properties of subject domains.
Though classical logics and its various extensions are widely used in com-
puter science [1] some restrictions of such logics should be mentioned. For
∗This work was supported in part by the project “Development of logic-algorithmic
methods for investigation of formal models of natural languages” of Taras Shevchenko
National University of Kyiv, Ukraine, Ref. Nr. 0116U004780.
2010 MSC: 03G25, 08A70, 03B70.
Key words and phrases: partial predicate, quasiary predicate, predicate algebra,
predicate logic, soundness, completeness.
264 Algebras and logics of partial quasiary predicates
example, in computer science partial and non-deterministic predicates
over complex data structures often appear. Therefore there is a need to
construct such logical systems that better reflect the above-mentioned
features. One of specific features for computer science is quasiarity of
predicates. Such predicates are partial predicates defined over partial
states (partial assignments) of variables and, consequently, they do not
have fixed arity. Conventional n-ary predicates can be considered as a
special case of quasiary predicates. Algebras of partial quasiary predicates
form a semantic base for logics of such predicates. More detailed account
on this topic can be found in [2, 3]. In these works we investigated basic
algebras of partial quasiary predicates and constructed corresponding
logics. But such algebras are not expressive enough to formulate some
important properties of quasiary predicates. Therefore here we consider
extended algebras and investigate their properties. This leads to a special
logic of quasiary predicates. For this logic based on extended algebras we
construct a sequent calculus and prove its soundness and completeness.
The logic construction, accepted here, consists of several phases: first,
we construct predicate algebras, terms of which specify the language of a
logic; then we define interpretation mappings and a consequence relation;
at last, we construct a calculus for the defined logic. This scheme of logic
construction determines a structure of the paper.
In Section 1 we define extended first-order algebras of quasiary predi-
cates and study their properties. In Sections 2 we define and investigate
an extended logic of quasiary predicates and irrefutability consequence
relation. In Section 3 a sequent calculus is constructed; its soundness and
completeness are proved. In the last section conclusions are formulated.
We use arrow
t
−→ (
p
−→) to denote the class of total (partial) mappings,
arrow ↓ (↑) to denote that a mapping is defined (undefined) on its
argument, and symbol ≡ to denote a strong equality.
1. Extended first-order algebras
of partial quasiary predicates
Let V be a nonempty set of variables (names). Let A be a set of basic
values (A 6= ∅). Given V and A, the class VA of nominative sets is defined
as the class of all partial mappings from V to A, thus, VA = V
p
−→ A.
Informally speaking, nominative sets represent states of variables.
Though nominative sets are defined as mappings, we follow mathe-
matical tradition and also use set-theoretic notation for these objects.
M. Nikitchenko, S. Shkilniak 265
In particular, the notation d = [vi 7→ ai | i ∈ I] describes a nomina-
tive set d; the notation vi 7→ ai ∈ d means that d(vi) is defined and
its value is ai (d(vi) ↓= ai). The main operation for nominative sets
is a total unary parametric renomination rv1,...,vn
x1,...,xn
: VA
t
−→ VA where
v1, . . . , vn, x1, . . . , xn ∈ V , v1, . . . , vn are distinct variables, n > 0, which
is defined by the following formula:
rv1,...,vn
x1,...,xn
(d) = [ v 7→ a | v 7→ a ∈ d, v /∈ {v1, . . . , vn}]
∪ [ vi 7→ ai | xi 7→ ai ∈ d, vi ∈ {v1, . . . , vn}].
Intuitively, given d this operation yields a new nominative set changing
the values of v1, . . . , vn to the values of x1, . . . , xn respectively. We also
use simpler notation for this formula: rv̄
x̄(d). Note that we treat parame-
ter v1,...,vn
x1,...,xn
as a total mapping from {v1, . . . , vn} into {x1, . . . , xn} thus
parameters obtained by pairs permutations are identical. We write x ∈ v̄
to denote that x is a variable from v̄; we write v̄ ∪ x̄ to denote the set of
variables that occur in the sequences v̄ and x̄.
Operation of deleting a component with a variable v from a nominative
set d is denoted d|−v. Notation d =−v d′ means that d−v = d′
−v.
The set of assigned variables (names) in d is defined by the formula
asn(d) = {v ∈ V | v 7→ a ∈ d for some a ∈ A}.
Let Bool = {F, T} be a set of Boolean values and let PrV
A = VA
p
−→
Bool be the set of all partial predicates over VA. Such predicates are called
partial quasiary predicates.
For p ∈ PrV
A the truth and falsity domains of p are respectively
T (p) = {d ∈ VA | p(d) ↓= T} and F (p) = {d ∈ VA | p(d) ↓= F}.
A variable u ∈ V is unessential for p if p(d) ≡ p(d′) for all d, d′ ∈ VA
such that d =−u d′.
Operations over PrV
A are called compositions. Basic compositions over
quasiary predicates with arity greater than 0 (non-trivial compositions) are
disjunction ∨, negation ¬, renomination Rv̄
x̄, and existential quantification
∃x. We extend them with null-ary (trivial) composition εx called variable
unassignment predicate. Thus, the extended set CE(V ) of first-order
compositions consists of compositions ∨, ¬, Rv̄
x̄, ∃x, εz for all parameters
x̄, v̄, x, z.
Compositions have the following types:
∨ : PrV
A × PrV
A
t
−→ PrV
A ; ¬, Rv̄
x̄, ∃x : PrV
A
t
−→ PrV
A , εx : PrV
A
266 Algebras and logics of partial quasiary predicates
and are defined by the following formulas (p, q ∈ PrV
A):
• T (p ∨ q) = T (p) ∪ T (q); F (p ∨ q) = F (p) ∩ F (q);
• T (¬p) = F (p); F (¬p) = T (p);
• T (Rv̄
x̄(p)) = {d ∈ VA | rv̄
x̄(d) ∈ T (p)};
F (Rv̄
x̄(p)) = {d ∈ VA | rv̄
x̄(d) ∈ F (p)};
• T (∃xp) = {d ∈ VA | d∇x 7→ a ∈ T (p) for some a ∈ A};
F (∃xp) = {d ∈ VA | d∇x 7→ a ∈ F (p) for all a ∈ A};
• T (εz) = {d ∈ VA | z /∈ asn(d)}; F (εz) = {d ∈ VA | z ∈ asn(d)}.
Here d∇x 7→ a = [v 7→ c ∈ d | v 6= x] ∪ [x 7→ a].
Please note that definitions of compositions are similar to strong
Kleene’s connectives and quantifiers.
A pair AQE(V, A) =< PrV
A ; CE(V ) > is called an extended first-order
algebra of partial quasiary predicates.
Let us consider semantic properties of such algebras. Compositions
∨, ¬, Rv̄
x̄, ∃x, εz specify four types of properties related to propositional
compositions ∨ and ¬, to renomination composition Rv̄
x̄, to existential
quantifier ∃x, and to variable unassignment composition (predicate) εz.
Properties of propositional compositions are traditional. In particular,
disjunction composition is associative, commutative, and idempotent;
negation composition is involutive ¬¬p = p.
Renomination composition is a new composition specific for logics
of quasiary predicates. Its properties are not well-known therefore we
describe them in more detail. We formulate six equalities (R∨, R¬, RR,
R∃, Rεs, Rε) for distributive properties and three equalities (R, RI, RU)
for normalization properties. Note, that here only those properties are
presented which will induce corresponding sequent rules.
Lemma 1. The following properties of renomination compositions hold:
R∨: Rv̄
x̄(p ∨ q) = Rv̄
x̄(p) ∨ Rv̄
x̄(q);
R¬: Rv̄
x̄(¬p) = ¬Rv̄
x̄(p);
RR: Rv̄
x̄(Rw̄
ȳ (p)) = Rv̄
x̄ ◦w̄
ȳ (p);
R∃: Rv̄
x̄(∃yp) = ∃zRv̄
x̄(Ry
z(p)), z /∈ v̄ ∪ {y}, z is unessential for p;
Rεs: Rv̄
x̄(εz) = εz, z 6∈ v̄;
Rε: Rv̄,z
x̄,y(εz) = εy;
R: R(p) = p;
RI: Rz,v̄
z,x̄(p) = Rv̄
x̄(p);
RU: Ry,v̄
z,x̄(p) = Rv̄
x̄(p), y is unessential for Rv̄
x̄(p).
Here Rv̄
x̄◦w̄
ȳ represents two successive renomination Rw̄
ȳ and Rv̄
x̄.
M. Nikitchenko, S. Shkilniak 267
Proof. We prove the lemma by showing that truth and falsity domains
for predicates in the left- and right-hand sides of equalities coincide. Let
us consider property R∃ only.
For the truth domain we have (d ∈ VA):
d ∈ T (Rv̄
x̄(∃yp)) ⇔ rv̄
x̄(d) ∈ T (∃yp) ⇔ rv̄
x̄(d)∇y 7→ a ∈ T (p) for some
a ∈ A ⇔ (rv̄
x̄(d)∇y 7→ a)∇z 7→ a ∈ T (p) for some a ∈ A (since z is
unessential for p) ⇔ (since z /∈ {y}) (rv̄
x̄(d)∇z 7→ a)∇y 7→ a ∈ T (p) for
some a ∈ A ⇔ (rv̄
x̄(d)∇z 7→ a) ∈ T (Ry
z(p)) for some a ∈ A ⇔ (since
z /∈ x̄) d∇z 7→ a ∈ T (Rv̄
x̄(Ry
z(p))) for some a ∈ A ⇔ d ∈ T (∃zRv̄
x̄(Ry
z(p))).
In the same way the coincidence of the falsity domains is proved.
As to variable unassignment composition (predicate), we admit that
εz is a total predicate (T (εy)∪F (εy) = VA) for which any y (y ∈ V, y 6= z)
is unessential.
Lemma 2. The following properties of quantification compositions hold
(x 6= y):
T∃v : T (Rx
y(p)) ∩ F (εy) ⊆ T (∃xp);
F∃v : F (∃xp) ∩ F (εy) ⊆ F (Rx
y(p));
T∃u : T (Rx
y(p)) ⊆ T (εy) ∪ T (∃xp);
F∃u : F (∃xp) ⊆ T (εy) ∩ F (Rx
y(p)).
Proof. To prove T∃v consider arbitrary d ∈ T (Rx
y(p))∩F (εy). This means
that y is assigned in d with some value a and d∇x 7→ a ∈ T (p), therefore
d ∈ T (∃xp).
Property F∃v is proved in the same manner.
Properties T∃u and F∃u are derived respectively from T∃v and F∃v
using equalities T (εy) ∪ F (εy) = VA and T (εy) ∩ F (εy) = ∅.
Algebras AQE(V, A) (for various A) form a semantic base for a pure
extended first-order logic of partial quasiary predicates LQE (called also
extended quasiary logic) being constructed here. Let us proceed with
formal definitions.
2. Extended quasiary logic
To define a logic we should define its semantic component, syntactic
component, and interpretational component [2, 3]. Semantics of the logic
under consideration is specified by algebras of the type AQE(V, A) (for
various A), so, we start with syntactic component of the logic.
268 Algebras and logics of partial quasiary predicates
2.1. Syntactic component
A syntactic component specifies the language of LQE . For simplicity,
we use the same notation for symbols of compositions and compositions
themselves. Let CEs(V ) be a set of composition symbols that represent
compositions in algebras defined above. Thus, CEs(V ) consists of symbols
∨, ¬, Rv̄
x̄, ∃x, εz for all parameters x̄, v̄, x, z.
Let Ps be a set of predicate symbols, V and U be infinite sets (U ⊆ V ).
U is called a set of unessential variables. This set does not affect the set of
formulas, but restricts their interpretations. Having U we obtain more pos-
sibilities for formula transformations. A tuple ΣQE = (V, U, CEs(V ), Ps)
is a language signature. Given ΣQE , we define inductively the language
of LQE – the set of formulas Fr(ΣQE). Formulas P and εz are atomic
(P ∈ Ps, z ∈ V ); composite formulas are of the form Φ∨Ψ, ¬Φ, Rv̄
x̄Φ, and
∃xΦ where Φ and Ψ are formulas. Formulas of the form Rv̄
x̄P (P ∈ Ps) are
called primitive. Such formula is normal [2] if none of the normalization
rules can be applied to it.
2.2. Interpretational component
Given ΣQE and nonempty set A we can define an extended algebra of
partial quasiary predicates AQE(V, A) =< PrV
A ; CE(V ) >. Composition
symbols have fixed interpretation. We also need interpretation IP s :
Ps
t
−→ PrV
A of predicate symbols; for obtained predicates all variables
u ∈ U should be unessential.
Formulas and interpretations in LQE are called LQE-formulas and
LQE-interpretations respectively. Usually the prefix LQE is omitted. Given
a formula Φ and an interpretation J we can speak of an interpretation of
Φ in J . It is denoted by ΦJ .
Predicates εz specify cases when z is assigned or unassigned. This
property can be used for construction of sequent rules for quantifiers.
Note that notation E!z in free logic [4] corresponds to negation of εz.
In the sequel we adopt the following convention: a, b denote elements
from A; x, y, s, z, v, w (maybe with indexes) denote variables (names) from
V ; d, d′, d1, d2 denote nominative sets from VA; p, q denote predicates from
AQE(V, A); P denotes a predicate symbol from Ps; Φ, Ψ, Ξ, Ω denote
LQE-formulas; Γ, ∆, Υ denotes sets of LQE-formulas; J denotes LQE-
interpretation. The set of all variables (names) that occur in Φ is denoted
nm(Φ). Variables from U\nm(Φ) are called fresh unessential variables for
Φ and their set is denoted fu(Φ). We use natural extensions of this notation
for a case of several formulas and sets of formulas like nm(Rū
v̄ , ∃xΦ, Γ, ∆)
M. Nikitchenko, S. Shkilniak 269
and fu(Rū
v̄ , ∃xΦ, Γ, ∆). A set ε(Γ) = {x | εx ∈ Γ} is the set of unassigned
variables in Γ → ∆ and ε(∆) = {x | εx ∈ ∆} is the set of assigned
variables in Γ → ∆. A set uns(Γ → ∆) = nm(Γ ∪ ∆) \ (ε(Γ) ∪ ε(∆)) is
the set of unspecified variables in Γ → ∆.
2.3. Consequence relation for sets of formulas
Let Γ ⊆ Fr(ΣQE) and ∆ ⊆ Fr(ΣQE) be sets of formulas. ∆ is a
consequence of Γ in interpretation J (denoted by Γ J |= ∆), if
⋂
Φ∈Γ
T (ΦJ) ∩
⋂
Ψ∈∆
F (ΨJ) = ∅.
This formula is also written in a simpler form as T (Γ) ∩ F (∆) = ∅.
∆ is a logical consequence of Γ (denoted by Γ |= ∆), if Γ J |= ∆ in every
interpretation J .
This relation of logical consequence is irrefutability relation.
Here we consider only those properties of the consequence relation
which induce sequent rules for the logic under consideration. Such proper-
ties are constructed upon semantic properties of compositions (Lemma 1,
Lemma 2). To do this the following lemma is often used.
Lemma 3. Let J be an arbitrary interpretation. Then
• if T (ΦJ) = T (ΨJ) then Φ, Γ J|= ∆ ⇔ Ψ, Γ J|= ∆;
• if F (ΦJ) = F (ΨJ) then Γ J|= Φ, ∆ ⇔ Γ J|= Ψ, ∆;
• if T (ΦJ) = T (ΨJ) ∩ T (Ω) then Φ, Γ J|= ∆ ⇔ Ψ, Ω, Γ J|= ∆;
• if F (ΦJ) = F (ΨJ) ∪ F (Ω) then
ΓJ|= Φ, ∆ ⇔ ΓJ|= Ψ, ∆ and ΓJ|= Ω, ∆.
Proof. Φ, Γ J |= ∆ means that T (ΦJ) ∩ T (ΓJ) ∩ F (∆J) = ∅. For the
first property this is equivalent to T (ΨJ) ∩ T (ΓJ) ∩ F (∆J) = ∅ since
T (ΦJ)=T (ΨJ). The last condition is equivalent to Ψ, Γ J|= ∆.
Other properties are proved in the same way.
Using this lemma we can prove the following properties:
∨L: Φ∨Ψ, Γ |= ∆ ⇔ Φ, Γ |= ∆ and Ψ, Γ |= ∆;
∨R: Γ |= ∆, Φ∨Ψ ⇔ Γ |= ∆, Φ, Ψ.
They induce sequent rules ∨L and ∨R (see the next section).
Lemma 4. Let u ∈ fu(Φ). Then for any interpretation J variable u is
unessential for ΦJ .
270 Algebras and logics of partial quasiary predicates
Proof goes by induction on the structure of Φ.
This result can be generalized on sets of formulas.
Lemma 5. The following properties related to quantification compositions
hold:
∃EL : ∃xΦ, Γ |= ∆ ⇔ Rx
z (Φ), Γ |= εz, ∆, if z ∈ fu(∃xΦ, Γ, ∆);
∃E1R : Γ |= ∃xΦ, εy, ∆ ⇔ Γ |= Rx
y(Φ), ∃xΦ, εy, ∆;
∃E2R : Γ |= ∃xΦ, ∆ ⇔ Γ |= Rx
z (Φ), εz, ∃xΦ, ∆,
if ε(∆) = ∅ and z ∈ fu(∃xΦ, Γ, ∆);
∃E3R : Γ |= ∃xΦ, ∆ ⇔ εy, Γ |= ∃xΦ, ∆ and Γ |= Rx
y(Φ), εy, ∃xΦ, ∆,
if y ∈ uns(Γ → ∆).
Proof. For ∃EL we should prove that
T (∃xΦJ) ∩ T (ΓJ) ∩ F (∆J) = ∅
⇔ T (Rx
z (Φ)J) ∩ T (ΓJ) ∩ F (εzJ) ∩ F (∆J) = ∅.
⇒) Let T (∃xΦJ )∩T (ΓJ )∩F (∆J ) = ∅. By T∃v, T (Rx
z (Φ)J )∩F (εzJ ) ⊆
T (∃xΦJ), therefore T (Rx
z (Φ)J) ∩ T (ΓJ) ∩ F (εzJ) ∩ F (∆J) = ∅.
⇐) Let T (Rx
z (Φ)J) ∩ T (ΓJ) ∩ F (εzJ) ∩ F (∆J) = ∅. Assume that
T (∃xΦJ) ∩ T (ΓJ) ∩ F (∆J) 6= ∅. Then there exists d such that d ∈
T (∃xΦJ) ∩ T (ΓJ) ∩ F (∆J). We have d ∈ T (∃xΦJ), d ∈ T (ΓJ), and
d ∈ F (∆J). Since d ∈ T (∃xΦJ) we have d∇x 7→ a ∈ T (ΦJ) for some
a ∈ A. But z ∈ fu(∃xΦ, Γ, ∆) therefore (d∇x 7→ a)∇z 7→ a ∈ T (ΦJ),
d∇z 7→ a ∈ T (ΓJ), and d∇z 7→ a ∈ F (∆J). Since (d∇x 7→ a)∇z 7→ a =
(d∇z 7→ a)∇x 7→ a, d∇z 7→ a ∈ T (Rx
z (Φ)J); by definition of εz we have
d∇z 7→ a ∈ F (εzJ), thus, d∇z 7→ a ∈ T (Rx
z (Φ)J) ∩ T (ΓJ) ∩ F (εzJ) ∩
F (∆J), that contradicts to the assumption.
For ∃E1R we should prove that
T (ΓJ) ∩ F (∃xΦJ) ∩ F (εy) ∩ F (∆J) = ∅
⇔ T (ΓJ) ∩ F (Rx
y(Φ)J) ∩ F (∃xΦJ) ∩ F (εy) ∩ F (∆J) = ∅
⇒) This part is obvious.
⇐) Let T (ΓJ )∩F (Rx
y(Φ)J )∩F (∃xΦJ )∩F (εy)∩F (∆J ) = ∅. Assume
that T (ΓJ )∩F (∃xΦJ )∩F (εy)∩F (∆J ) 6= ∅. Then there exists d such that
d ∈ T (ΓJ )∩F (∃xΦJ )∩F (εy)∩F (∆J ). We have d ∈ T (ΓJ ), d ∈ F (∃xΦJ ),
d ∈ F (εy), and d ∈ F (∆J). Since d ∈ F (εy) then y 7→ a ∈ d for some a.
Since d ∈ F (∃xΦJ) then d∇x 7→ a ∈ F (ΦJ). Therefore d ∈ F (Rx
y(Φ)J),
that contradicts to the assumption.
M. Nikitchenko, S. Shkilniak 271
For ∃E2R we should prove that
T (ΓJ) ∩ F (∃xΦJ) ∩ F (∆J) = ∅
⇔ T (ΓJ) ∩ F (Rx
z (Φ)J) ∩ F (εzJ) ∩ F (∃xΦJ) ∩ F (∆J) = ∅.
⇒) This part is obvious.
⇐) The proof of this part goes similar to proof of ∃EL. Assuming
that d ∈ T (ΓJ) ∩ F (∃xΦJ) ∩ F (∆J) we prove that for any a a new
d′ = d∇z 7→ a belongs to T (ΓJ )∩F (Rx
z (Φ)J )∩F (εzJ )∩F (∃xΦJ )∩F (∆J ),
that contradicts to the assumption.
Property ∃E3R is proved in the same manner.
3. Sequent calculus for LQE
For the logic LQE we build a calculus of sequent type. Sequents are
pairs of the form Γ → ∆, where Γ and ∆ are countable sets of formulas.
Formulas of Γ are called T -formulas of the sequent, formulas of ∆ are
called F -formulas.
Semantic properties of relation |= have their syntactic analogues –
sequent rules. If a rule has additional condition (sometimes denoted C) it
is written on the right of the rule. We present three groups of sequent
rules associated with three groups of non-trivial compositions.
Sequent rules for propositional compositions:
∨L
Φ, Γ → ∆ Ψ, Γ → ∆
Φ ∨ Ψ, Γ → ∆
; ∨R
Γ → Φ, Ψ, ∆
Γ → Φ ∨ Ψ, ∆
;
¬L
Γ → Φ, ∆
¬Φ, Γ → ∆
; ¬R
Φ, Γ → ∆
Γ → ¬Φ, ∆
.
Sequent rules for renomination compositions:
R∨L
Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ), Γ → ∆
Rv̄
x̄(Φ ∨ Ψ), Γ → ∆
; R∨R
Γ → Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ), ∆
Γ → Rv̄
x̄(Φ ∨ Ψ), ∆
;
R¬L
¬Rv̄
x̄(Φ), Γ → ∆
Rv̄
x̄(¬Φ), Γ → ∆
; R¬R
Γ → ¬Rv̄
x̄(Φ), ∆
Γ → Rv̄
x̄(¬Φ), ∆
;
RRL
Rv̄
x̄ ◦w̄
ȳ (Φ), Γ → ∆
Rv̄
x̄(Rw̄
ȳ (Φ)), Γ → ∆
; RRR
Γ → Rv̄
x̄ ◦w̄
ȳ (Φ), ∆
Γ → Rv̄
x̄(Rw̄
ȳ (Φ)), ∆
;
R∃L
∃uRv̄
x̄Ry
u(Φ), Γ → ∆
Rv̄
x̄(∃yΦ), Γ → ∆
, CR∃; R∃R
Γ → ∃uRv̄
x̄Ry
u(Φ), ∆
Γ → Rv̄
x̄(∃yΦ), ∆
, CR∃;
272 Algebras and logics of partial quasiary predicates
RεsL
εz, Γ → ∆
Rv̄
x̄(εz), Γ → ∆
, z /∈ v̄; RεsR
Γ → εz, ∆
Γ → Rv̄
x̄(εz), ∆
, z /∈ v̄;
RεL
εy, Γ → ∆
Rv̄,z
x̄,y(εz), Γ → ∆
;
RεR
Γ → εy, ∆
Γ → Rv̄,z
x̄,y(εz), ∆
;
RL
Φ, Γ → ∆
R(Φ), Γ → ∆
; RR
Γ → Φ, ∆
Γ → R(Φ), ∆
;
RIL
Rv̄
x̄(Φ), Γ → ∆
Rz,v̄
z,x̄(Φ), Γ → ∆
;
RIR
Γ → Rv̄
x̄(Φ), ∆
Γ → Rz,v̄
z,x̄(Φ), ∆
;
RUL
Rv̄
ū(Φ), Γ → ∆
Ry,v̄
z,ū(Φ), Γ → ∆
, CRU; RUR
Γ → Rv̄
ū(Φ), ∆
Γ → Ry,v̄
z,ū(Φ), ∆
, CRU.
Here CR∃ is u ∈ fu(Rv̄
x̄(∃yΦ)), CRU is y ∈ fu(Φ).
Sequent rules for quantification compositions:
∃EL
Rx
z (Φ), Γ → εz, ∆
∃xΦ, Γ → ∆
, z ∈ fu(∃xΦ, Γ, ∆);
∃E1R
Γ → Rx
y(Φ), ∃xΦ, εy, ∆
Γ → ∃xΦ, εy, ∆
;
∃E2R
Γ → Rx
z (Φ), εz, ∃xΦ, ∆
Γ → ∃xΦ, ∆
, ε(∆) = ∅, z ∈ fu(∃xΦ, Γ, ∆);
∃E3R
εy, Γ → ∃xΦ, ∆ Γ → Rx
y(Φ), εy, ∃xΦ, ∆
Γ → ∃xΦ, ∆
, y ∈ uns(Γ → ∆).
Rule ∃E1R is applied when at least one variable is assigned. Rule
∃E2R is applied when there are no assigned variables (in this case a fresh
unassigned variables is assigned). This means the first application of
quantification elimination (therefore ε(∆) = ∅). Rule ∃E3R is applied
when an unspecified variable is involved into quantifier elimination. In
this case two branches appear: with this variable being unassigned and
assigned.
The above written rules specify QE-calculus.
Based on definition of |= and properties of compositions we obtain
the following properties for sequent rules of QE-calculus.
M. Nikitchenko, S. Shkilniak 273
Lemma 6. Let
Γ′ → ∆′
Γ → ∆ and
Γ′ → ∆′ Γ′′ → ∆′′
Γ → ∆ be sequent rules of
QE-calculus. Then
Γ′ |= ∆′ ⇔ Γ |= ∆; Γ′ |= ∆′ and Γ′′ |= ∆′′ ⇔ Γ |= ∆.
To define derivability in QE-calculus we should first introduce the
notion of closed sequent. Such sequents are axioms of QE-calculus. For
QE-calculus we have two conditions for a sequent to be closed:
• classical closedness (c-closedness);
• unassigned closedness (u-closedness).
Classical closedness is defined in a usual way: sequent Γ → ∆ is closed
if there exists Φ such that Φ ∈ Γ and Φ ∈ ∆.
Unassigned closedness is defined in more difficult way. Given sequent
Γ → ∆ and Rr1,..,rk,x1,..,xn,z1,..zm
s1,..,sk,y1,...,yn,v1,...,vm
Φ such that {x1, . . . , xn}∩ε(Γ) = ∅ and
{r1, . . . , rk, s1, . . . , sk, y1, . . . , yn} ⊆ ε(Γ), an expression Rx1,...,xn,z1,...,zm
⊥, ..., ⊥,v1,...,vm
Φ
is called a ⊥-form of Rr1,..,rk,x1,..,xn,z1,..,zm
s1,..,sk,y1,...,yn,v1,...,vm
Φ. Then we define two formulas
Rv̄
x̄(Φ) and Rs̄
ȳ(Φ) be u-equivalent with respect to Γ → ∆ if their ⊥-
forms coincide. At last, we say that Γ → ∆ is u-closed if there exist
two u-equivalent formulas Rv̄
x̄(Φ) and Rs̄
ȳ(Φ) such that Rv̄
x̄(Φ) ∈ Γ and
Rs̄
ȳ(Φ) ∈ ∆.
Lemma 7. If Γ → ∆ is closed then Γ |= ∆.
Proof. To prove this lemma we should consider two cases: Γ |= ∆ is c-
closed or u-closed. For the first case the lemma is obvious. Assume that
Γ → ∆ is u-closed. Then Γ → ∆ can be presented in the form ε(Γ),
Rv̄
x̄(Φ), Σ → Υ, Rs̄
ȳ(Φ), where Rv̄
x̄(Φ) and Rs̄
ȳ(Φ) are u-equivalent.
Let J be an interpretation and d ∈ VA. Two cases are possible:
• εuJ(d) = T for all u ∈ ε(Γ);
• εuJ(d) = F for some u ∈ ε(Γ).
For the first case Rv̄
x̄(Φ)J(d) ≡ Rs̄
ȳ(Φ)J(d) by u-equivalence, therefore
d /∈ T (Rv̄
x̄(Φ)J) ∩ F (Rs̄
ȳ(Φ)J); for the second case d /∈ T (ε(ΓJ)).
Since d was chosen arbitrarily we have that
T (ε(ΓJ)) ∩ T (Rv̄
x̄(Φ)J) ∩ T (ΣJ) ∩ F (ΥJ) ∩ F (Rs̄
ȳ(Φ)J) = ∅.
J was chosen arbitrarily therefore ε(Γ), Rv̄
x̄(Φ), Σ |= Υ, Rs̄
ȳ(Φ). This
means that Γ |= ∆.
Derivation in QE-calculus has the form of tree, the vertices of which
are sequents. Such trees are called sequent trees. A sequent tree is closed,
274 Algebras and logics of partial quasiary predicates
if every its leaf is a closed sequent. A sequent Γ → ∆ is derivable, if
there is a closed sequent tree with the root Γ → ∆. Sequent calculus is
constructed in such a way that a sequent Γ → ∆ has a derivation if and
only if Γ |= ∆.
Let us consider a procedure of construction of the sequent tree for a
given sequent Γ →∆. Such procedure is defined in the same way as for
other sequent calculi for countable sequents [5] therefore we present only
its general description without details. In the case of logic of quasiary
predicates, the procedure of construction of a sequent tree is more compli-
cated. The reason is that the value of a predicate p on d can be different
depending on whether the component with some variable is assigned in d
or not. Therefore sets of assigned, unassigned, and unspecified variables
should be examined. This feature manifests itself in the sequent rules
∃E1R, ∃E2R, and ∃E3R.
During construction of a sequent tree the following cases are possible:
• all sequents on the leaves are closed; we have a finite closed tree;
• procedure is not completed; we have a finite or infinite unclosed
tree. Such tree has at least one path called unclosed all vertices of
which are unclosed sequents.
The first case leads to soundness of QE-calculus.
Theorem 1 (soundness). Let Γ → ∆ be derivable. Then Γ |= ∆.
Proof. If Γ → ∆ is derivable then a finite closed tree was constructed.
By the procedure of sequent tree construction we have that for any leaf
of this tree its sequent Γ′ → ∆′ is closed. Thus, by Lemma 7, Γ′ |= ∆′
holds. By Lemma 6, sequent rules preserve relation of logical consequence.
Therefore for the root of the tree Γ → ∆ we also have that Γ |= ∆.
For the second case, formulas of the unclosed path form Hintikka’s
model for which a counter example can be constructed. To do this we
first formulate the properties of formulas of an unclosed path.
Let ℘ be an unclosed path in a sequent tree, L and R be respectively
sets of all T -formulas and F -formulas of sequents of a path ℘.
All sequents of the path ℘ are unclosed, therefore the c- and u-
closedness conditions are not satisfied. From this follows unclosedness
conditions of a pair H = (L, R):
HC) for every Φ it is not possible that Φ ∈ L and Φ ∈ R;
HCU) there does not exist a pair of u-equivalent formulas of the form
Rv̄
x̄Φ and Rū
ȳΦ such that Rv̄
x̄Φ ∈ L and Rū
ȳΦ ∈ R.
M. Nikitchenko, S. Shkilniak 275
Let W = nm(L ∪ R) \ ε(L). We assume that W 6= ∅; the case with
W = ∅ can be considered as in propositional logic.
For our derivation procedure the following conditions, derived from
the sequent rules of QE-calculus, should hold.
H∨) If Φ ∨ Ψ ∈ L then Φ ∈ L or Ψ ∈ L;
if Φ ∨ Ψ ∈ R then Φ ∈ R and Ψ ∈ R.
H¬) If ¬Φ ∈ L then Φ ∈ R; if ¬Φ ∈ R then Φ ∈ L.
HR∨) If Rv̄
x̄(Φ ∨ Ψ) ∈ L then Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ) ∈ L;
if Rv̄
x̄(Φ ∨ Ψ) ∈ R then Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ) ∈ R.
HR¬) If Rv̄
x̄(¬Φ) ∈ L then ¬Rv̄
x̄(Φ) ∈ L;
if Rv̄
x̄(¬Φ) ∈ R then ¬Rv̄
x̄(Φ) ∈ R.
HRR) If Rv̄
x̄(Rw̄
ȳ (Φ)) ∈ L then Rv̄
x̄ ◦w̄
ȳ (Φ) ∈ L;
if Rv̄
x̄(Rw̄
ȳ (Φ)) ∈ R then Rv̄
x̄ ◦w̄
ȳ (Φ) ∈ R.
HR∃) If Rv̄
x̄(∃yΦ) ∈ L then ∃zRv̄
x̄Ry
z(Φ) ∈ L for some z ∈ fu(Rv̄
x̄(∃xΦ));
if Rv̄
x̄(∃yΦ) ∈ R then ∃zRv̄
x̄Ry
z(Φ) ∈ R for some z ∈ fu(Rv̄
x̄(∃xΦ)).
HRεs) If Rv̄
x̄(εz) ∈ L and z /∈ v̄ then εz ∈ L;
if Rv̄
x̄(εz) ∈ R and z /∈ v̄ then εz ∈ R.
HRε) If Rv̄,z
x̄,y(εz) ∈ L then εy ∈ L; if Rv̄,z
x̄,y(εz) ∈ R then εz ∈ R.
HR) If R(Φ) ∈ L then Φ ∈ L; if R(Φ) ∈ R then Φ ∈ R.
HRI) If Rz,v̄
z,x̄(Φ) ∈ L then Rv̄
x̄(Φ) ∈ L; if Rz,v̄
z,x̄(Φ) ∈ R then Rv̄
x̄(Φ) ∈ R.
HRU) If Ry,v̄
z,x̄(Φ) ∈ L and y ∈ fu(Rv̄
x̄(Φ)) then Rv̄
x̄(Φ) ∈ L;
if Ry,v̄
z,x̄(Φ) ∈ R and y ∈ fu(Rv̄
x̄(Φ)) then Rv̄
x̄(Φ) ∈ R.
H∃) If ∃xΦ ∈ L then there exists y ∈ W such that Rx
y(Φ) ∈ L;
if ∃xΦ ∈ R then Rx
y(Φ) ∈ R for every y ∈ W .
Let us demonstrate the correctness of the last property. Indeed, let
∃xΦ ∈ L, then on some derivation step of path ℘ the ∃EL rule was applied
to T -formula ∃xΦ giving T -formula Rx
y(Φ). Therefore Rx
y(Φ) ∈ L and
εy ∈ R, thus y ∈ W . So, for some y ∈ W we have Rx
y(Φ) ∈ L.
Dually, let ∃xΦ ∈ R; take any y ∈ W . Then necessarily one of the
rules ∃E1R, ∃E2R, or ∃E3R was applied to ∃xΦ with such y generating a
formula Rx
y(Φ) ∈ R. Note that in the rule ∃E3R the first branch generates
a formula εy ∈ L, thus, such y /∈ W .
A pair of formula sets H = (L, R), for which the above formulated
conditions (with letter ’H’ in their labels) hold, is called a quasiary model
pair, or quasiary Hintikka’s pair.
A pair (L, R) of arbitrary sets of formulas is called satisfiable if there
exist a set A, an interpretation J , and δ ∈ VA such that:
• for all Φ ∈ L ΦJ(δ) ↓= T ;
• for all Φ ∈ R ΦJ(δ) ↓= F .
276 Algebras and logics of partial quasiary predicates
Lemma 8. Let H = (L, R) be a quasiary Hintikka’s pair. Then H is
satisfiable.
Proof. Given such pair H = (L, R), we construct an extended quasiary
algebra, an interpretation in this algebra, and a nominative set that
confirm satisfiability of H.
Choose any set A such that |A| = |W |. The set A “mimics” W . This
specifies an algebra AQE(V, A).
Let δ ∈ VA be such data that asn(δ) = W and δ itself (considered as
a mapping) realizes a bijection from W to A.
First, we prescribe interpretation of variable unassignment predicates
according to their definition:
• if εy ∈ L then define εyJ(δ) = T (this means that y /∈ asn(δ)),
• if εy ∈ R then define εyJ(δ) = F (this means that y ∈ asn(δ)).
Then we prescribe interpretation to predicates symbols. Values of
corresponding predicates are determined by atomic and normal primitive
formulas. Also, unessential variables should be taken into account.
Atomic formulas of the form P where P ∈ Ps define
• PJ(δ) = T if P ∈ L,
• PJ(δ) = F if P ∈ R.
Normal primitive formulas of the form Rv̄
x̄(P ) define
• PJ(rv̄
x̄(δ)) = T if Rv̄
x̄(P ) ∈ L,
• PJ(rv̄
x̄(δ)) = F if Rv̄
x̄(P ) ∈ R.
Also, we extend predicate interpretations specifying variables from U
as unessential.
The predicates are defined unambiguously due to unclosedness condi-
tions HC and HCU.
Indeed, for the case of atomic formula P this follows from HC, for the
case of two different normal primitive formulas Rv̄
x̄P and Rū
ȳP we obtain
different nominative sets rv̄
x̄(δ) and rū
ȳ (δ), thus, no ambiguity can arise.
The proof goes on by induction on the formula structure with respect
to definition of H = (L, R).
For atomic and normal primitive formulas the satisfiability statements
follow from their definitions.
Let us prove induction steps for these statements. We consider the
main cases only and omit simpler cases.
Let Φ ∨ Ψ ∈ L. By H∨ we have Φ ∈ L or Ψ ∈ L. By induction
hypothesis ΦJ(δ) = T or ΨJ(δ) = T , therefore (Φ ∨ Ψ)J(δ) = T . Let
Φ ∨ Ψ ∈ R. By H∨ we have Φ ∈ R and Ψ ∈ R. By induction hypothesis
ΦJ(δ) = F and ΨJ(δ) = F , therefore (Φ ∨ Ψ)J(δ) = F .
M. Nikitchenko, S. Shkilniak 277
Let Rv̄
x̄(Φ∨Ψ) ∈ L. By HR∨ we have Rv̄
x̄(Φ)∨Rv̄
x̄(Ψ) ∈ L. By induction
hypothesis (Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ))J(δ) = T , therefore (Rv̄
x̄(Φ ∨ Ψ))J(δ) = T .
Let Rv̄
x̄(Φ ∨ Ψ) ∈ R. By HR∨ we have Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ) ∈ R. By induction
hypothesis(Rv̄
x̄(Φ) ∨ Rv̄
x̄(Ψ))J(δ) = F , therefore (Rv̄
x̄(Φ ∨ Ψ))J(δ) = F .
Let Rv̄
x̄(∃yΦ) ∈ L. By HR∃ we have ∃zRv̄
x̄Ry
z(Φ) ∈ L, where z ∈
fu(Rv̄
x̄(∃xΦ)). By induction hypothesis (∃zRv̄
x̄Ry
z(Φ))J(δ) = T , therefore
(Rv̄
x̄(∃yΦ))J (δ) = T . Let Rv̄
x̄(∃yΦ) ∈ R. By HR∃ we have ∃zRv̄
x̄Ry
z(Φ) ∈ R,
where z ∈ fu(Rv̄
x̄(∃Φ)). By induction hypothesis (∃zRv̄
x̄Ry
z(Φ))J(δ) = F ,
therefore (Rv̄
x̄(∃yΦ))J(δ) = F .
Let ∃xΦ ∈ L. By H∃ there exists y ∈ W such that Rx
y(Φ) ∈ L. By
induction hypothesis (Rx
y(Φ))J(δ) = T . From this ΦJ(δ∇x 7→ δ(y)) = T .
But δ(y) ↓ according to δ ∈ W A and y ∈ W , therefore for a = δ(y) we
have ΦJ(δ∇x 7→ a) = T , thus, (∃xΦ)J(δ) = T . Let ∃xΦ ∈ R. By H∃ for
all y ∈ W we have Rx
y(Φ) ∈ R. By induction hypothesis (Rx
y(Φ))J (δ) = F
for all y ∈ W . From this ΦJ (δ∇x 7→ δ(y)) = F for all y ∈ W . By δ ∈ WA,
we have δ(y) ↓ for all y ∈ W . Since δ is a bijection W → A, then every
b ∈ A can be represented in the form b = δ(y) for some y ∈ W . So,
ΦJ (δ∇x 7→ b) = F for every b ∈ A, therefore we have (∃xΦ)J (δ) = F .
Theorem 2 (completeness). Let Γ |= ∆. Then Γ → ∆ is derivable.
Proof. Assume that Γ |= ∆ and Γ → ∆ is not derivable. In this case a
derivation tree for Γ → ∆ is not closed. Thus, an unclosed path ℘ exists in
this derivation tree. Let L and R be respectively the sets of all T -formulas
and F -formulas of this path. By Lemma 8, H = (L, R) is satisfiable for
some set A, some interpretation J , and some δ ∈ VA. This means that
ΦJ(δ) = T for all Φ ∈ L and ΦJ(δ) = F for all Φ ∈ R. Since Γ ⊆ L and
∆ ⊆ R, then for all Φ ∈ Γ we have ΦJ(δ) = T and for all Ψ ∈ ∆ we have
ΨJ(δ) = F . This contradicts to Γ |= ∆.
QE-calculus is a new generalized version of QG-calculus presented
in [6]. QG-calculus was constructed for a basic quasiary logic with special
rather complicated consequence relation, but here we adopted a traditional
definition of this relation.
The obtained results can be used in logics for program reasoning. Some
steps of construction of such quasiary program logics were presented in [7].
Conclusion
In the paper we have investigated algebras and logics defined for
classes of partial quasiary predicates. Quasiary predicates and quasiary
278 Algebras and logics of partial quasiary predicates
functions are used to represent semantics of computer programs and their
components. Based on algebras of such predicates we have defined a corre-
sponding extended quasiary logic with irrefutability consequence relation.
A sequent calculus has been constructed for this logic, its soundness and
completeness have been proved.
References
[1] Handbook of Logic in Computer Science, S. Abramsky, Dov M. Gabbay, and T. S.
E. Maibaum (eds.), in 5 volumes, Oxford Univ. Press, Oxford, 1993–2001.
[2] M. Nikitchenko, V. Tymofieiev, Satisfiability in Composition-Nominative Logics,
Central European Journal of Computer Science, vol. 2, issue 3, 2012, pp. 194-213.
[3] M. Nikitchenko, S. Shkilnyak, Applied Logic, Publishing house of Taras Shevchenko
National University of Kyiv, Kyiv, 2013 (in Ukrainian), 278 p.
[4] E. Bencivenga, Free Logics, in Handbook of Philosophical Logic, D. Gabbay and F.
Guenthner (eds.), vol. III: Alternatives to Classical Logic, Dordrecht: D. Reidel,
1986, pp. 373–426.
[5] J. Gallier, Logic for computer science: foundations of automatic theorem proving.
Second edition, Dover, New York, 2015.
[6] S. S. Shkilniak, First-order logics of quasiary predicates, Kibernetika I Sistemnyi
Analiz, 6, 2010 (in Russian), pp. 32-50.
[7] A. Kryvolap, M. Nikitchenko, W. Schreiner, Extending Floyd-Hoare logic for partial
pre- and postconditions, CCIS, vol. 412, Springer, Heidelberg, 2013, pp. 355-378.
Contact information
M. Nikitchenko,
S. Skilniak
Taras Shevchenko National University of Kyiv;
64/13, Volodymyrska Street, City of Kyiv,
Ukraine, 01601
E-Mail(s): mykola.nikitchenko@gmail.com,
sssh@unicyb.kiev.ua
Web-page(s): http://ttp.unicyb.kiev.ua/
Received by the editors: 06.04.2017
and in final form 06.06.2017.
|