|
-
Ключові слова:
класична логіка, классическая логика ; логіка предикатів, логика предикатов, predicate logic ; математична логіка, математическая логика ; мови програмування, языки программирования, computer program language
-
Анотація:
В роботі визначаються монотонні логіки Флойда-Хоара на базі багатоосновних алгебр часткових квазіарних предикатів та програм. Для цієї цілі дається визначення спеціальної, монотонної композиції Флойда-Хоара. Доводиться, що означена композиція є також неперервною. Будуються правила виводу в монотонних логіках, які отримуються з правил виводу логіки Флойда-Хоара за допомогою додавання до правил відповідних обмежень. Доводиться коректність системи правил виводу та необхідність додаткових обмежень, що накладаються на них.
Based on many-sorted algebras of partial quasiary predicates and programs monotone Floyd-Hoare logics are defined. For this purpose definition of special monotone Floyd-Hoare composition is given. Specified composition is proved to be also continuous. Rules of inference in monotone logic, which are obtained from rules of inference for Floyd-Hoare logic, are constructed. Their validity and the need of additional restrictions imposed on them are proved.
-
Є складовою частиною документа:
-
Теми документа
-
Окремі фонди та колекції КНУ // праці авторів КНУТШ, труды авторов КНУТШ, работы авторов КНУТШ
|
