**Authors:** Mykola Nikitchenko, Oksana Shkilniak, Stepan Shkilniak, Tohrul Mamedov

**Keywords:** partial predicate, quasiary predicate, program
logic, predicate logic, soundness and completeness.

### Abstract

Partial quasiary predicates are used in programming for rep-
resenting program semantics and in logic for formalizing predi-
cates over partial variable assignments. Such predicates do not
have fixed arity therefore they may be treated as mappings over
partial data. Obtained logics are not expressive enough to con-
struct sound axiomatic systems of Floyd–Hoare type. To increase
expressibility of such logics, oriented on quasiary predicates, we
extend their language with the complement operation (composi-
tion). In the paper we define one of such logics called first-order
logic of partial quasiary predicates with the complement com-
position. For this logic a special consequence relation called ir-
refutability consequence relation under undefinedness conditions
is introduced. We study its properties, construct a sequent calcu-
lus for it and prove soundness and completeness of this calculus.

Taras Shevchenko National University of Kyiv, Ukraine

E-mail:

### Fulltext

–

0.18 Mb