Pure first-order quasiary logics with equality predicates

M.S. Nikitchenko, S.S. Shkilniak

Abstract


Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are studied. The main attention is paid to logics with special equality   relations. Logics with weak equality and strong equality are defined, their properties are investigated. Languages of such logics and their interpetations are described.  The following classes of interpretations (semantics) are identified: partial deterministic, non-deterministic, total deterministic, and total non-deterministic interpetations. Semantic properties of the proposed logics are investigated. Special attention is paid to consequence relations for sets of formulas. Based on the properties of these relations a number of calculi of sequent type is proposed. Basic rules of these calculi and corresponding closedness conditions are formulated; the procedure of sequent tree construction is described. For the proposed calculi correctness and completeness theorems are proved. The proof of completeness is based on the construction of countermodel for an unclosed path in the sequent tree.

Problems in programming 2017; 2: 03-23


Keywords


logic; predicate; equality; logical consequence; sequent calculus

References


ABRAMSKY S., GABBAY D. and MAIBAUM T. (editors). (1993–2000). Handbook of Logic in Computer Science Modal logic. Oxford University Press.

NIKITCHENKO M. and SHKILNIAK S. (2008). Mathematical logic and theory of algorithms. Кyiv: VPC Кyivskyi Universytet (in ukr).

NIKITCHENKO M. and SHKILNIAK S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr).

NIKITCHENKO M. and SHKILNIAK S. (2015). Semantic Properties of Logics of Quasiary Predicates. In Workshop on Foundations of Informatics: Proceedings FOI-2015. Chisinau, Moldova. P. 180–197.

NIKITCHENKO M. and SHKILNIAK S. (2016). Pure first-order logics of quasiary predicates. In Problems in Progamming. N 2–3. P. 73–86 (in ukr).

SHKILNIAK S. and VOLKOVYTSKYI D. (2014). Renominative composition-nominative logics with predicates of equality. In Bulletin of Taras Shevchenko National University of Kyiv. Series: Physics & Mathematics. N 3. P. 198–205 (in ukr).

SHKILNIAK S. and VOLKOVYTSKYI D. (2016). Renominative logics of quasiary predicates. In Computer mathematics. 1. P. 46–57 (in ukr).

SHKILNIAK О. (2017). Logical consequence relations in logics of monotone predicates and logics of antitone predicates. In Problems in Progamming. N 1. P. 21–29 (in ukr).

SHKILNIAK S. (2013). Spectrum of sequent calculi of first-order composition-nominative logics. In Problems in Progamming. N 3, P. 22–37 (in ukr).




DOI: https://doi.org/10.15407/pp2017.02.003

Refbacks

  • There are currently no refbacks.