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

• Пинько Олексій Павлович (фізико-математичні науки)

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"