Логіки, орієнтовані на специфікації програм - Нікітченко, М.С.; Шкільняк, С.С.; Омельчук, Л.Л. (Інститут програмних систем НАН України, 2006)
Розглянуті композиційно-номінативні логіки, орієнтовані на специфікації програм. Такі логіки будуються в семантико-
синтаксичному стилі на основі композиційно-номінативного підходу. Пропонується спектр композиційно-номінативних логік
різних рівнів абстрактності та загальності. Для логік еквітонних квазіарних предикатів на основі секвенційних числень доведені тео-
реми про визначність. На базі аксіоматичної системи специфікацій програм над метаномінативними даними побудовано прототип
системи автоматизації доведення теорем теорії МНД. Composition nominative logics oriented on program specification are considered. Such logics based on composition nominative approach
are constructed in a semantic-syntactic style. The spectrum of logics of various abstraction and generality levels is developed. The definability
theorems are proved based on the sequent calculi for logics of equitone quasiare predicates. The prototype of automatic theorem
prover is constructed for the axiomatic system of program specification over metanominative data.