Київський Вісник Київського національного університету імені Тараса Шевченка / Київський, університет імені національний; редкол.: голов. ред. Анісімов А.В. ; Хусаінов Д.Я., Arturs Medvids, Miklos Ronto [та ін.]. - Київ, 2016
Анотація:
Досліджено логіки часткових квазіарних предикатів безкванторнo-функціональних рівнів. Виділено різновиди таких логік із композиціями слабкої рівності та строгої рівності. Описано семантичні моделі й мови цих логік, досліджено їх семантичні властивості, запропоновано низку числень секвенційного типу. На базі теорем повноти цих числень для таких логік отримано розв"язність проблем наявності логічного наслідку для скінчених множин формул, істинності й виконуваності формул.
In this paper we study new classes of program-oriented logical formalisms - logics of partial quasi-ary predicates of free-quantifier levels. These logics occupy intermediate position between propositional logic and first-order composition-nominative logics. We consider three classes of this logics: free-quantifier functional logics (FQFL), free-quantifier functional logics with composition of weak equality = (FQFLE) and free-quantifier functional logics with composition of strong equality ? (FQFLSE). We define semantic models and languages of the introduced logics and consider their semantic properties. We describe properties of the composition superposition, weak equality and strong equality. We consider normal forms of terms and formulas, properties of logical consequence rela&tions for sets of formulas. These properties form the semantic base for construction a number of sequent type calculi for logics of free-quantifier levels. On the base of the completeness theorem of sequent calculi we obtain an algorithmic solvabilit&y of problems for free-quantifier logics: problems of existence of logical consequence for finite sets of formulas, irrefutability problems and identically truth problems for formulas.
