Pure first-order quasiary logics with equality predicates

• Veröffentlicht in: PROBLEMS IN PROGRAMMING
• Datum: 2018
• Heft: 2
• Сторінки: 3-23
• ISSN: 1727-4907
• Автори та афіліації: M.S. Nikitchenko — Kiev Taras Shevchenko National University; S.S. Shkilniak — Kiev Taras Shevchenko National University
• Ключові слова: логічний наслідок, логіка, рівність, секвенційне числення, рівноправність, логічні міркування, предикативність, предикація, рівновага, то- чка рівноваги
• Hauptverfasser: Nikitchenko, M.S., Shkilniak, S.S.
• Format: Artikel
• Sprache: Ukrainisch
• Veröffentlicht: PROBLEMS IN PROGRAMMING 2018
• Schlagworte: logic; predicate; equality; logical consequence; sequent calculus; UDC 004.42:510.69
• Online Zugang: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/316
• Назва журналу: Problems in programming

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