Описано метод субімплікант, розроблений для мінімізації логічних функцій, що приймають не менше трьох значень. Метод відзначається покращанням результатів мінімізації за рахунок розширення умов склеювання та можливістю мінімізації функцій, що не піддаються мінімізації традиційними способами.

Індекс рубрикатора НБУВ: В128.2

Рубрики:

Багатозначна логіка

Шифр НБУВ: Ж14024 Пошук видання у каталогах НБУВ 

Представлено можливості побудови секвенційних числень без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності (тобто скінченною множиною унарних похідних пропозиційних зв'язок зі спеціальною властивістю). Такі числення складаються з аксіом, до яких належать тільки літери, та оборотних правил виведення, які вводять комплекси пропозиційних зв'язок. Інтерпретуючи секвенції атомарними формулами першого порядку, відзначено, що зазначені числення можна інтерпретувати точними універсальними Хорновськими теоріями. В цьому випадку процедура цілеспрямованого виведення для даних теорій, що реалізована в таких системах програмування, як АПС або Пролог, імітує процедуру оберненого виведення в зазначених численнях.

Встановлено двоїстість істиннісних значень як інваріантність пари цих значень відносно циклічної групи перетворень другого порядку. Таку двоїстість введено в систему пропозиційних зв'язок, формул та контекстів логіки висловлень.

Індекс рубрикатора НБУВ: В128.2

Рубрики:

Багатозначна логіка

Шифр НБУВ: Ж15477 Пошук видання у каталогах НБУВ 

Визначено монотонні логіки Флойда - Хоара на базі багатоосновних алгебр часткових квазіарних предикатів та програм. Для цієї цілі надано визначення спеціальної, монотонної композиції Флойда - Хоара. Доведено, що означена композиція є також неперервною. Побудовано правила виводу в монотонних логіках, які одержуються з правил виводу логіки Флойда - Хоара за допомогою додавання до правил відповідних обмежень. Доведено коректність системи правил виводу та необхідність додаткових обмежень, що накладаються на них.

A general method of constructing the sequent calculi with cut elimination property for propositional finitely valued logics with equality determinant is proposed.

Logical criteria of the algebraizability of sequent calculi for propositional finitely valued logics with an equality determinant are obtained.

Algebraic criteria of the algebraizabihty of sequential calculi for finitely valued logics with equality determinant are obtained.

Terminated proof procedures in axiomatic extensions of sequent calculi for propositional finitely valued logics with equality determinant are proposed on the basis of logic programming.

The derivable rules of axiomatic extensions of sequent calculi with structural rules for the prepositional finitely valued logics with an equality determinant are analyzed with the use of methods of logic programming.

Запропоновано ефективну процедуру мінімізації числа засновків правил введення секвенційних числень для пропозиційних скінченнозначних логік із визначником рівності.

Предложен новый метод минимизации числа переменных в полных и неполных логических функциях, основанный на процедуре расцепления конъюнктермов. Преимущества предложенного метода показаны на примерах определения несущественных переменных в функциях, заимствованных автором из известных публикаций в порядке сравнения.