Секвенціальні системи виведення для багатозначних логік

В цій роботі представлено, як можна побудувати секвенціальні числення без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності (тобто скінченною множиною унарних похідних пропозиційних зв’язок...

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2003
Автор:	Пинько, О.П.
Формат:	Стаття
Мова:	Ukrainian
Опубліковано:	Інститут проблем математичних машин і систем НАН України 2003
Теми:	Програмно-технічні комплекси
Онлайн доступ:	https://nasplib.isofts.kiev.ua/handle/123456789/731
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:	Секвенціальні системи виведення для багатозначних логік / Пинько О.П. // Математичні машини і системи. – 2003. – № 2. – С. 166 – 174.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	nasplib_isofts_kiev_ua-123456789-731
record_format	dspace
spelling	Пинько, О.П. 2008-06-24T13:31:52Z 2008-06-24T13:31:52Z 2003 Секвенціальні системи виведення для багатозначних логік / Пинько О.П. // Математичні машини і системи. – 2003. – № 2. – С. 166 – 174. 1028-9763 https://nasplib.isofts.kiev.ua/handle/123456789/731 510.6 В цій роботі представлено, як можна побудувати секвенціальні числення без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності (тобто скінченною множиною унарних похідних пропозиційних зв’язок зі спеціальною властивістю). Такі числення складаються з аксіом, до яких належать тільки літери, та оборотних правил виведення, які вводять комплекси пропозиційних зв’язок. Інтерпретуючи секвенції атомарними формулами першого порядку, ми відзначаємо, що зазначені числення можна інтерпретувати точними універсальними Хорновськими теоріями. При цьому процедура цілеспрямованого виведення для даних теорій, що реалізована в таких системах програмування, як АПС або Пролог, імітує процедуру оберненого виведення в зазначених численнях. Бібліогр.: 16 назв. В этой работе представлено, как можно построить секвенциальные исчисления без структурных правил (но с допустимыми структурными правилами) для произвольных пропозициональных конечнозначных логик с определителем равенства (т.е. конечным множеством унарных производных пропозициональных связок со специальным свойством). Такие исчисления состоят из аксиом, в которые входят только литералы, и обратимых правил вывода, которые вводят комплексы пропозициональных связок. Интерпретируя секвенции атомарными формулами первого порядка, мы показываем, что указанные исчисления можно интерпретировать точными универсальными Хорновскими теориями. При этом процедура целенаправленного вывода для таких теорий, которая реализована в таких системах программирования, как АПС или Пролог, имитирует процедуру обратного вывода в указанных исчислениях. Библиогр.: 16 назв. In this paper we show how one can construct sequential calculi without structural rules (but with admissible structural rules) for arbitrary propositional finitely-valued logics with an identity determinant (that is, a finite set of unary secondary propositional connectives with a special property). Such calculi consist of axioms containing literals alone and invertible inference rules introducing complex propositional connectives. Interpreting sequents by atomic first-order formulas, we show that such calculi can be interpreted by strict universal Horn theories. Moreover, the procedure of goal-oriented deduction for such theories implemented in such programming systems as APS or Prolog simmulates the procedure of inverse deduction in the mentioned calculi. Refs.: 16 titles. uk Інститут проблем математичних машин і систем НАН України Програмно-технічні комплекси Секвенціальні системи виведення для багатозначних логік Секвенциальные системы вывода для многозначных логик Sequential systems of deduction for many-valued logic Article published earlier
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
title	Секвенціальні системи виведення для багатозначних логік
spellingShingle	Секвенціальні системи виведення для багатозначних логік Пинько, О.П. Програмно-технічні комплекси
title_short	Секвенціальні системи виведення для багатозначних логік
title_full	Секвенціальні системи виведення для багатозначних логік
title_fullStr	Секвенціальні системи виведення для багатозначних логік
title_full_unstemmed	Секвенціальні системи виведення для багатозначних логік
title_sort	секвенціальні системи виведення для багатозначних логік
author	Пинько, О.П.
author_facet	Пинько, О.П.
topic	Програмно-технічні комплекси
topic_facet	Програмно-технічні комплекси
publishDate	2003
language	Ukrainian
publisher	Інститут проблем математичних машин і систем НАН України
format	Article
title_alt	Секвенциальные системы вывода для многозначных логик Sequential systems of deduction for many-valued logic
description	В цій роботі представлено, як можна побудувати секвенціальні числення без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності (тобто скінченною множиною унарних похідних пропозиційних зв’язок зі спеціальною властивістю). Такі числення складаються з аксіом, до яких належать тільки літери, та оборотних правил виведення, які вводять комплекси пропозиційних зв’язок. Інтерпретуючи секвенції атомарними формулами першого порядку, ми відзначаємо, що зазначені числення можна інтерпретувати точними універсальними Хорновськими теоріями. При цьому процедура цілеспрямованого виведення для даних теорій, що реалізована в таких системах програмування, як АПС або Пролог, імітує процедуру оберненого виведення в зазначених численнях. Бібліогр.: 16 назв. В этой работе представлено, как можно построить секвенциальные исчисления без структурных правил (но с допустимыми структурными правилами) для произвольных пропозициональных конечнозначных логик с определителем равенства (т.е. конечным множеством унарных производных пропозициональных связок со специальным свойством). Такие исчисления состоят из аксиом, в которые входят только литералы, и обратимых правил вывода, которые вводят комплексы пропозициональных связок. Интерпретируя секвенции атомарными формулами первого порядка, мы показываем, что указанные исчисления можно интерпретировать точными универсальными Хорновскими теориями. При этом процедура целенаправленного вывода для таких теорий, которая реализована в таких системах программирования, как АПС или Пролог, имитирует процедуру обратного вывода в указанных исчислениях. Библиогр.: 16 назв. In this paper we show how one can construct sequential calculi without structural rules (but with admissible structural rules) for arbitrary propositional finitely-valued logics with an identity determinant (that is, a finite set of unary secondary propositional connectives with a special property). Such calculi consist of axioms containing literals alone and invertible inference rules introducing complex propositional connectives. Interpreting sequents by atomic first-order formulas, we show that such calculi can be interpreted by strict universal Horn theories. Moreover, the procedure of goal-oriented deduction for such theories implemented in such programming systems as APS or Prolog simmulates the procedure of inverse deduction in the mentioned calculi. Refs.: 16 titles.
issn	1028-9763
url	https://nasplib.isofts.kiev.ua/handle/123456789/731
citation_txt	Секвенціальні системи виведення для багатозначних логік / Пинько О.П. // Математичні машини і системи. – 2003. – № 2. – С. 166 – 174.
work_keys_str_mv	AT pinʹkoop sekvencíalʹnísistemivivedennâdlâbagatoznačnihlogík AT pinʹkoop sekvencialʹnyesistemyvyvodadlâmnogoznačnyhlogik AT pinʹkoop sequentialsystemsofdeductionformanyvaluedlogic
first_indexed	2025-12-07T17:15:05Z
last_indexed	2025-12-07T17:15:05Z
_version_	1850870548567949312

Секвенціальні системи виведення для багатозначних логік

Репозитарії

Схожі ресурси