Özet:

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.

Anahtar Kelimeler: