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

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

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2003
Автор:	Пинько, О.П.
Формат:	Стаття
Мова:	Ukrainian
Опубліковано:	Інститут проблем математичних машин і систем НАН України 2003
Теми:	Програмно-технічні комплекси
Онлайн доступ:	http://dspace.nbuv.gov.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	irk-123456789-731
record_format	dspace
spelling	irk-123456789-7312008-06-25T12:00:18Z Секвенціальні системи виведення для багатозначних логік Пинько, О.П. Програмно-технічні комплекси В цій роботі представлено, як можна побудувати секвенціальні числення без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності (тобто скінченною множиною унарних похідних пропозиційних зв’язок зі спеціальною властивістю). Такі числення складаються з аксіом, до яких належать тільки літери, та оборотних правил виведення, які вводять комплекси пропозиційних зв’язок. Інтерпретуючи секвенції атомарними формулами першого порядку, ми відзначаємо, що зазначені числення можна інтерпретувати точними універсальними Хорновськими теоріями. При цьому процедура цілеспрямованого виведення для даних теорій, що реалізована в таких системах програмування, як АПС або Пролог, імітує процедуру оберненого виведення в зазначених численнях. Бібліогр.: 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. 2003 Article Секвенціальні системи виведення для багатозначних логік / Пинько О.П. // Математичні машини і системи. – 2003. – № 2. – С. 166 – 174. 1028-9763 http://dspace.nbuv.gov.ua/handle/123456789/731 510.6 uk Інститут проблем математичних машин і систем НАН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Ukrainian
topic	Програмно-технічні комплекси Програмно-технічні комплекси
spellingShingle	Програмно-технічні комплекси Програмно-технічні комплекси Пинько, О.П. Секвенціальні системи виведення для багатозначних логік
description	В цій роботі представлено, як можна побудувати секвенціальні числення без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності (тобто скінченною множиною унарних похідних пропозиційних зв’язок зі спеціальною властивістю). Такі числення складаються з аксіом, до яких належать тільки літери, та оборотних правил виведення, які вводять комплекси пропозиційних зв’язок. Інтерпретуючи секвенції атомарними формулами першого порядку, ми відзначаємо, що зазначені числення можна інтерпретувати точними універсальними Хорновськими теоріями. При цьому процедура цілеспрямованого виведення для даних теорій, що реалізована в таких системах програмування, як АПС або Пролог, імітує процедуру оберненого виведення в зазначених численнях. Бібліогр.: 16 назв.
format	Article
author	Пинько, О.П.
author_facet	Пинько, О.П.
author_sort	Пинько, О.П.
title	Секвенціальні системи виведення для багатозначних логік
title_short	Секвенціальні системи виведення для багатозначних логік
title_full	Секвенціальні системи виведення для багатозначних логік
title_fullStr	Секвенціальні системи виведення для багатозначних логік
title_full_unstemmed	Секвенціальні системи виведення для багатозначних логік
title_sort	секвенціальні системи виведення для багатозначних логік
publisher	Інститут проблем математичних машин і систем НАН України
publishDate	2003
topic_facet	Програмно-технічні комплекси
url	http://dspace.nbuv.gov.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
first_indexed	2025-07-02T04:23:14Z
last_indexed	2025-07-02T04:23:14Z
_version_	1836507668321140736
fulltext	ISSN 1028-9763. Математичні машини і системи, 2003, № 2 166 УДК 510.6 О.П. ПИНЬКО________________________________________________________________________ СЕКВЕНЦІАЛЬНІ СИСТЕМИ ВИВЕДЕННЯ ДЛЯ БАГАТОЗНАЧНИХ ЛОГІК Вступ Проблема організації взаємодії людини та комп’ютерної системи часто нерозривно пов’язана з розв’язанням логічних задач (наприклад, в експертних системах, які грунтуються на логічному підході до обробки знань, або в системах автоматичного доведення теорем, які використуються для розв’язання логічних задач в математиці), що зробило досить актуальним (в межах зазначеної проблеми) питання розробки систем автоматичного виведення в відповідних логічних численнях. Особливе місце при цьому займає аналіз різноманітних некласичних логік, які були б більш придатні для моделювання міркувань у різних предметних галузях і могли б бути використані в інформатиці. Існує два основних засоби введення некласичних логік. Перший – синтаксичний – полягає у підборі придатного числення, яке б відрізнялося від класичного (наприклад, шляхом вилучення або послаблення аксіом, або правил виведення класичного числення). Другий – семантичний – полягає у використанні більш ніж двох істинносних значень, що привело до виникнення поняття багатозначної логіки. Залишаючи питання про численні використання нескінченнозначних логік, таких, як нечітка (або неперервна) логіка, ми лише нагадаємо тут про корисність деяких скінченнозначних логік в межах інформатики. По-перше, як відомо, для комп’ютерних систем характерна неповнота інформації, що приводить до доцільності використання певних конструктивних логік (наприклад, трьохзначної логіки Клині) в різних системах машинного виведення. Крім того, у комп’ютерних системах, в які інформація може надходити з декількох незалежних джерел, можлива наявність несумісної (суперечної) інформації, обробка якої на засадах класичної або конструктивної логіки призводила б до повного руйнування накопиченої корисної інформації [3]. Тому більш доцільно використовувати, наприклад, трьохзначні паранесуперечні логіки замість класичної двохзначної або чотирьохзначні – замість трьохзначної логіки Клині. Існують також інші цікаві варіанти багатозначних логік (з більшою кількістю істинносних значень), які ми тут не обговорюємо докладно. Однією з основних задач щодо багатозначних логік (особливо у зв’язку з автоматизацією виведення та застосуванням до інформатики) є пошук їх аксіоматизацій, які були б придатні для комп’ютерної реалізації процедур автоматичного доведення теорем. У роботах [4, 5] була запропонована секвенціальна аксіоматизація LK класичної логіки, різні модифікації якої потім знайшли широке застосування при автоматизації виведення в цій (двохзначній) логіці. Щодо багатозначних логік, то узагальнюючи генценовську ідею двохмісцевої секвенції, у роботах [6, 7] було запропоновано використовувати багатомісцеві секвенції. В зазначених статтях були розроблені загальні методи побудови m-місцевих секвенціальних числень для довільних m-значних логік, де 2≥m . Далі ця ідея зазнала певних модифікацій та узагальнень [8]. Однак звичайні двохмісцеві секвенціальні числення були б краще для аксіоматизації відношень логічного наслідування в некласичних логіках, оскільки метавираз “формула ϕ є логічним наслідком скінченної множини формул Γ” можна інтерпретувати двохмісцевою секвенцією ϕ→Г , в той час, як щодо багатомісцевих секвенцій така інтерпретація (якщо вона взагалі існує) значно більш громіздка. Проте, незважаючи на побудову генценовських числень для певних некласичних логік (наприклад, інтуїціоністської), питання про придатність генценовського двохмісцевого секвенціального формалізму взагалі до багатозначних логік залишилося не вивченим в літературі. ISSN 1028-9763. Математичні машини і системи, 2003, № 2 167 В цій роботі ми вивчаємо скінченнозначні логіки з визначником рівності. Клас таких логік включає до складу (як зліченні підкласи) клас усіх двохзначних логік (при цьому =ℑ ∅), клас усіх трьох- и чотирьохзначних логік зі слабким запереченням ¬ (при цьому { }¬=ℑ ), класи усіх скінченнозначних логік Лукасевича і Поста, а також клас усіх скінченнозначних функціонально повних логік (див. підрозділи 2.1, 2.2 та 2.3 відповідно). В розділі 2 ми показуємо, як можна побудувати двохмісцеві секвенціальні числення без структурних правил для довільних багатозначних логік з визначником рівності. На відміну від числення LK [4, 5] та числень, розглянутих в [6, 7] і оглянутих в [8], наші числення містять, крім правил уведення зв’язок, також правила уведення “комплексів зв’язок” (ідея використовувати такі правила веде походження від роботи Попова [9]), тобто формул вигляду ( )( )nv ϕϕµ ,...,1 , де ℑ∈v , µ – n-арна зв’язка (де, в свою чергу, 0≥n , а nϕϕ ,...,1 – пропозиційні формули. Загальний підхід, запропонований в цій роботі, охоплює деякі конкретні числення, що введені нами раніше в роботах [10, 11, 12]. Секвенції можна інтерпретувати атомарними формулами першого порядку. Таким чином, секвенціальні числення трактуються як точні універсальні Хорновські теорії. Це надає можливість використовувати програмні системи, які мають вбудовані процедури уніфікації та цілеспрямованого логічного виведення (такі, як Пролог та АПС [1, 2]), для реалізації процедур виведення в численнях, що розглядаються. Це питання докладно обговорюється у розділі 3. Основні поняття та позначення Ми дотримуємося звичайних алгебраїчних понять [13]. Щоб уніфікувати позначення, алгебри позначатимуться жирними курсивними великими латинськими літерами (можливо, з індексами), а їх носії – відповідними курсивними великими латинськими літерами (з тими ж індексами). (Абстрактна) пропозиційна мова – це довільна алгебраїчна сигнатура L, символи (тобто операції) якої трактуються як (пропозиційні) зв’язки. Зафіксуємо зліченну множину { } 0≥= iipV , елементи якої називатимуться пропозиційними змінними або атомами. Абсолютно вільна L-алгебра з системою вільних твірних V позначається FL. Елементи FL називаються (пропозиційними) L-формулами. Якщо A – L-алгебра, то інтерпретацією в A називається усякий гомоморфізм із FL в A. (Як звичайно, інтерпретації в алгебрах ототожнюються з їх обмеженнями на множину V або навіть на його підмножини, що складаються з “суттєвих” пропозиційних змінних. При цьому ми іноді використовуємо такі позначення інтерпретацій, як [ ]nn avav /,...,/ 11 , де nvv ,...,1 – пропозиційні змінні, а naa ,...,1 – елементи алгебри, що розглядається). Інтерпретації в FL називаються L-підстановками. (Багатозначна) L-логіка – це довільна пара вигляду ( )DAM ,= , де A – L-алгебра, елементи якої називаються її (істинносними) значеннями, а AD ⊆ (елементи D називаються відзначеними (істинносними) значеннями M). Відношення (логічного) наслідування MCn логіки M визначається як оператор замикання на множині LF таким чином [14]. Для усіх LFX ⊆ та LF∈ϕ установимо ( )XCnM∈ϕ т.т.т.к., для кожної інтерпретації h в A, [ ] ( ) .DhDXh ∈⇒⊆ ϕ L-Секвенція – це довільна пара скінченних множин Γ і ∆ L-формул, яка записується у вигляді ∆→Г . Поняття (секвенціального) правила, його посилки та висновку, оберненого правила, (секвенціальної) аксіоми, (секвенціального) числення, виведення в численні та секвенції, що має виведення в численні, визначаються, як звичайно. ISSN 1028-9763. Математичні машини і системи, 2003, № 2 168 L-Секвенція ∆→Г називається істинною в M при інтерпретації h в A, якщо [ ] [ ] ≠∩∆⇒⊆ DhDГh ∅, і хибною у противному разі [15]. L-Правило називається (логічно) загальнозначимим в M, якщо при будь-якій інтерпретації в A одна з його посилок хибна в M або його висновок істинний в M [12]. Відзначимо, що усі структурні правила (включаючи переріз) загальнозначимі в M [12]. 2. Секвенціальні числення для логік з визначником рівності Зафіксуємо скінченну пропозиційну мову L та скінченнозначну логіку ( )DAM ,= , таку, що ∅ AD ≠≠ . Визначником рівності для M називається така множина ℑ унарних похідних зв’язок, крім p0, що для будь-яких a, Ab∈ , таких, що ba ≠ та DaDa ∈⇔∈ , існує таке ℑ∈v , що ( ) ( ) DbvDav ∉⇔∈ . Далі ми уводимо скінченну синтаксичну конструкцію (визначення 1), яка пов’язана з M і ℑ та використовується потім для побудови відповідних секвенціального числення (визначення 2 та теорема 2) і скінченної точної універсальної Хорновської теорії першого порядку без рівності (розділ 3), та доводимо її існування (теорема 1). Спочатку ми уводимо узагальнене поняття літери. Нехай VW ⊆ . W-Літера – це будь-який елемент множини ( ){ }WwvwvW ∈ℑ∈∪ ,\| . Множина усіх W-літер позначається ( )WLit . V-Літери називаються просто літерами. Секвенція ∆→Г називається (W-) літерною, якщо ∆∪Г складається з (W-)літер. Визначення 1. Секвенціальна ( )L,ℑ -таблиця для M – це будь-яка пара ( )ρλ,=Т відображень множини ( ) ( )ℑ×∪ℑ LL \ в множину скінченних множин літерних секвенцій, таких, що для усіх 0≥n і кожної n-арної L∈µ : 1) якщо ℑ∉µ , то ( )µλ і ( )µρ складаються з { }npp ,...,1 -літерних секвенцій, таких, що для усіх Aaa n ∈,...,1 , ( ) Daa n ∈,...,1µ т.т.т.к. деяка секвенція із ( )µλ хибна в M при інтерпретації [ ]nn apap /,...,/ 11 в A т.т.т.к. кожна секвенція із ( )µρ істинна в M при інтерпретації [ ]nn apap /,...,/ 11 в A; 2) для усіх ℑ∈v , ( )v,µλ і ( )v,µρ складається з { }npp ,...,1 -літерних секвенцій, таких, що для усіх Aaa n ∈,...,1 , ( )( ) Daav n ∈,...,1µ т.т.т.к. деяка секвенція із ( )v,µλ хибна в M при інтерпретації [ ]nn apap /,...,/ 11 в A т.т.т.к. кожна секвенція із ( )v,µρ істинна в M при інтерпретації [ ]nn apap /,...,/ 11 в A. Теорема 1. Теорема існування. Існує секвенціальна ( )L,ℑ -таблиця для M. Доведення: спочатку уведемо певні корисні позначення. Розглянемо довільні Aa∈ та ni ≤≤1 . Множину усіх { }ip -літер γ , таких, що [ ] ( )DDapi ∉∈/γ , позначимо ( ) ( )( )aNaP ii відповідно). Відзначимо, що ( ) [ ] DbpaPba ii ∈∈∀⇔= /:γγ та ( ) [ ] DbpaN ii ∉∈∀ /:γγ (1) для усіх Ab∈ . ISSN 1028-9763. Математичні машини і системи, 2003, № 2 169 Розглянемо довільні 0≥n та n-арну L∈µ . Спочатку розглянемо довільну ℑ∈v . Ураховуючи (1), ми бачимо, що ( ) ( ) ( ) ( )( ){ }DavAaaaNaPv niiniiini ∈∈∪→∪= ≤≤≤≤ 1111 ,,...,\|:, µµλ – скінченна множина { }npp ,...,1 -літерних секвенцій, таких, що для усіх ( )( ) DaavAaa nn ∈∈ ,...,,,..., 11 µ т.т.т.к. деяка секвенція із ( )v,µλ хибна в M при інтерпретації [ ]nn apap /,...,/ 11 в A. Аналогічно ( ) ( ) ( ) ( )( ){ }DavAaaaNaPv niiniiini ∉∈∪→∪= ≤≤≤≤ 1111 ,,...,\|:, µµρ – скінченна множина { }npp ,...,1 -літерних секвенцій, таких, що для усіх ( )( ) DaavAaa nn ∈∈ ,...,,,..., 11 µ т.т.т.к. кожна секвенція із ( )v,µρ істинна в M при інтерпретації [ ]nn apap /,...,/ 11 в A. Далі припустимо, що ℑ∉µ . Тоді, ураховуючи (1), ми бачимо, що ( ) ( ) ( ) ( ){ }DaaAaaaNaP nniiniiini ∈∈∪→∪= ≤≤≤≤ ,...,,,...,\|:, 1111 µµλ – скінченна множина { }npp ,...,1 -літерних секвенцій, таких, що для усіх ( ) DaaAaa nn ∈∈ ,...,,,..., 11 µ т.т.т.к. деяка секвенція із ( )µλ хибна в M при інтерпретації [ ]nn apap /,...,/ 11 в A. Аналогічно ( ) ( ) ( ) ( ){ }DaaAaaaNaP nniiniiini ∉∈∪→∪= ≤≤≤≤ ,...,,,...,\|:, 1111 µµρ – скінченна множина { }npp ,...,1 -літерних секвенцій, таких, що для усіх ( ) DaaAaa nn ∈∈ ,...,,,..., 11 µ т.т.т.к. кожна секвенція із ( )µρ істинна в M при інтерпретації [ ]nn apap /,...,/ 11 в A. Таким чином, отримано секвенціальну ( )L,ℑ -таблицю ( )ρλ,=T для M.  Відзначимо, що доведення теореми 1 є конструктивним. Ефективна процедура, яку можна витягти з нього, надає можливість знайти секвенціальну таблицю, яка, у свою чергу, є структурою вхідних даних для ефективної процедури мінімізації секвенціальних таблиць, що буде подана в іншій роботі. Визначення 2. Нехай ( )ρλ,=T – секвенціальна ( )L,ℑ -таблиця для M. Числення ( )TMC , складається з таких аксіом та правил: 1) для кожної Vw∈ , довільних скінченних множин літер Г і ∆ , кожної { }0p -літерної секвенції Ξ→Θ , що загальнозначима в M, аксіома [ ] [ ]wpwpГ // 00 Ξ∪∆→Θ∪ ; 2) для кожного 0≥n , кожної n-арної ℑ∈ /Lµ , довільних формул nϕϕ ,...,1 та довільних скінченних множин формул Г і ∆ правило з посилками вигляду [ ] [ ]nnnn ppppГ ϕϕϕϕ /,...,//,...,/ 1111 Ξ∪∆→Θ∪ , де ( )µλ∈Ξ→Θ , і висновком ( ){ } ∆→∪ nГ ϕϕµ ,...,1 та правило з посилками вигляду [ ] [ ]nnnn ppppГ ϕϕϕϕ /,...,//,...,/ 1111 Ξ∪∆→Θ∪ , де ( )µρ∈Ξ→Θ , і висновком ( ){ }nГ ϕϕµ ,...,1∪∆→ ; 3) для кожного 0≥n , кожної n-арної L∈µ , кожної ℑ∈v , довільних формул nϕϕ ,...,1 та довільних скінченних множин формул Г і ∆ правило з посилками вигляду [ ] [ ]nnnn ppppГ ϕϕϕϕ /,...,//,...,/ 1111 Ξ∪∆→Θ∪ , де ( )v,µλ∈Ξ→Θ , і висновком ( )( ){ } ∆→∪ nvГ ϕϕµ ,..,1 та правило з посилками вигляду ISSN 1028-9763. Математичні машини і системи, 2003, № 2 170 [ ] [ ]nnnn ppppГ ϕϕϕϕ /,...,//,...,/ 1111 Ξ∪∆→Θ∪ , де ( )v,µρ∈Ξ→Θ , і висновком ( )( ){ }nvГ ϕϕµ ,...,1∪∆→ . Наступна теорема узагальнює відповідні теореми коректності та повноти, що доведені у [10, 11, 12]. Теорема 2. Теорема коректності та повноти. Нехай ( )ρλ,=T – секвенціальна ( )L,ℑ -таблиця для M. Тоді секвенція має виведення в численні ( )TMC , т.т.т.к., вона загальнозначима в M. Доведення: узагальнює доведення відповідних тверджень із [11, 12]. (Через те, що заміна головних зв’язок похідними зберігає загальнозначимість секвенцій та належність аксіом і правил до відповідних версій числення ( )TMC , , досить довести теорему 2 тільки для випадку, коли ℑ складається з головних зв’язок.) Відзначимо, що усі правила ( )TMC , та правила, що обернені до них, є загальнозначимими в M. Зокрема, ми безпосередньо отримаємо доведення необхідності. Достатність доведемо індукцією за ступенем ∂ секвенцій, який визначається таким чином. Спочатку визначимо ступінь ∂ формул індукцією за їх складністю, установлюючи: - ( ) ( )( ) 0:: =∂=∂ wvw , де Vw∈ та ℑ∈v ; - ( )( ) ( )( )( ) ( ) ( )( )( )iininn v ϕηϕϕϕµϕϕµ η ∂∑+∂∑+=∂=∂ ℑ∈≤≤111 1:,...,:,..., , де ℑ∈ /Lµ , ℑ∈v та nϕϕ ,...,1 – довільні формули; - ( )( )( ) ( ) ( )( )ϕηϕϕµ η ∂∑+∂+=∂ ℑ∈1:v , де ℑ∈v,µ та ϕ – довільна формула. (Відзначимо, що ( ) 0=∂ ϕ , де ϕ – довільна формула, т.т.т.к. ϕ – літера.) Далі, для довільної секвенції ∆→Г , установимо ( ) ( ) ( )ψϕ ψϕ ∂∑+∂∑=∆→∂ ∆∈∈ГГ : . (Відзначимо, що ( ) 0=∆→∂ Г т.т.т.к. секвенція ∆→Г – літерна.) Розглянемо довільну секвенцію Π→Λ , що загальнозначима в M. Спочатку припустимо, що ( ) 0=Π→Λ∂ . Від супротивного доведемо, що для деякої Vw∈ секвенція { }( )( ) { }( )( )wLitwLit ∩Π→∩Λ є загальнозначимою в M. Припустимо, що для усіх Vw∈ існує інтерпретація wh в A, при якій { }( )( ) { }( )( )wLitwLit ∩Π→∩Λ хибна в M. Визначимо інтерпретацію h в A, установлюючи ( ) ( )whwh w=: для усіх Vw∈ . Очевидно, що секвенція Π→Λ хибна в M при інтерпретації h . Це суперечить її загальнозначимості в M. Таким чином, існує така Vw∈ , що секвенція { }( )( ) { }( )( )wLitwLit ∩Π→∩Λ загальнозначима в M. Установимо { }( )( )[ ]0/: pwwLit∩Λ=Θ та { }( )( )[ ]0/: pwwLit∩Π=Ξ . Тоді { }0p−Ξ→Θ -літерна секвенція, яка загальнозначима в M. Таким чином, згідно з визначенням 2.1), установлюючи { }( )wLitГ \: Λ= та { }( )wLit\: Π=∆ , ми бачимо, що Π→Λ – аксіома числення ( )TMC , , тому вона, очевидно, має виведення в ньому. Далі припустимо, що ( ) 0>Π→Λ∂ . Тоді існує Π∪Λ∈ψ , яка не є літерою. В цьому разі існують 0≥n , формули nϕϕ ,...,1 та n -арна L∈µ , такі, що або ℑ∉µ і ( )nϕϕµψ ,...,1= , або ( )( )nv ϕϕµψ ,...,1= для деякої ℑ∈v . Припустимо, що Λ∈ψ (випадок, коли Π∈ψ розглядається аналогічно). Згідно з визначенням 2.2)-3), установлюючи { }ψ\: Λ=Г та Π=∆ : , ми бачимо, що ( )TMC , ISSN 1028-9763. Математичні машини і системи, 2003, № 2 171 містить правило з висновком Π→Λ та посилками, ступінь яких менше, ніж ( )Π→Λ∂ . Усі посилки такого правила загальнозначимі в M. Тоді, за індукційним припущенням, усі посилки цього правила мають виведення в ( )TMC , . Таким чином, його висновок Π→Λ також має виведення в ( )TMC , .  Відзначимо, що доведення теореми 2 конструктивне. Ефективна процедура, яку можна витягти з нього і яка використовує (як структуру вхідних даних) деяку секвенціальну таблицю (що знайдена теоретично або отримана внаслідок мінімізації), дає алгоритм розв’язання проблеми існування виведення секвенції в численні, що задається визначенням 2 у випадку, коли ℑ складається з головних зв’язок (розділ 3). Зазначимо декілька корисних наслідків теореми 2, які узагальнюють відповідні результати робіт [10, 11, 12]. Насамперед, використовуючи теорему 2 та теорему компактності щодо скінченнозначних логік [14], ми робимо висновок, що відношення наслідування M аксіоматизується численням ( )TMC , у такому розумінні. Наслідок 1. Для усіх LFX ⊆ та LF∈ϕ , ( )XCnM∈ϕ т.т.т.к. існує скінченна XГ ⊆ , така, що секвенція ϕ→Г має виведення в ( )TMC , . Далі відзначимо декілька синтаксичних властивостей числення ( )TMC , , які можна легко довести, використовуючи теорему 2. Наслідок 2. Структурні правила (включаючи переріз), допустимі в ( )TMC , . Наслідок 3. Правила числення ( )TMC , оборотні. Завершуючи цей розділ, ми зазначимо декілька нескінченних (зліченних) класів скінченнозначних логік, до яких придатний наш підхід. 2.1. Двохзначні логіки. Нехай { }tfA ,:= и { }tD =: . Тоді ℑ = ∅ – визначник рівності для M. Єдиною { }0p -літерною секвенцією, що загальнозначима в M, є { } { }00 pp → . У разі класичної логіки можна легко підібрати ( )ℑ,L -секвенціальну таблицю T для M, таку, що ( )TMC , є добре відомою версією числення Генцена LK [4, 5]. 2.2. Трьох- і чотирьохзначні логіки зі слабким запереченням. Нехай унарна зв’язка слабкого заперечення { } { } { } DnDtDfbtADbntfAtfL ∉¬∉¬∈¬∩=⊆⊂∈¬ ,,,,:,,,,,, (якщо An∈ ) та Db∈¬ (якщо Ab∈ ). Тоді { }¬=ℑ – визначник рівності для M. Єдиними { }0p -літерними секвенціями, що загальнозначимі в M, є { } { }00 pp → , ∅ { }00 , pp ¬→ (т.т.т.к. An∉ ) та { }→¬ 00 , pp ∅ (т.т.т.к. Ab∉ ). Цей клас логік охоплює чотирьохзначну логіку Белнапа [3], їх різноманітні розширення, які вивчалися у [12] (включаючи логіку, що аксіоматизується численням Попова [9]), трьохзначну логіку Клині, суперінтуїціоністську трьохзначну логіку Гьоделя [16], трьохзначні паранесуперечливі логіки та багато інших. У роботах [10, 11, 12] були уведені та вивчені числення щодо деяких із зазначених логік (або їх фрагментів). Ці числення можна отримати із певних таблиць, використовуючи визначення 2. Зазначені роботи містять також результати, які випливають з теореми 2 та наслідків 1, 2 і 3. 2.3. Скінченнозначні логіки Лукасевича та Поста. Нехай { }⊃∨∧¬=≥ ,,,:,2 Ln , де ⊃∨∧¬ ,,, – зв’язки заперечення, кон’юнкції, диз’юнкції та імплікації відповідно, M – n-значна логіка Лукасевича з множиною істинносних значень { }1,...,0: −= nA , множиною відзначених істинносних значень { }1: −= nD і операціями, що визначені таким чином: ( ) ( )babababaana ,max:,,min:,1: =∨=∧−−=¬ і ( )1,1min: −+−=⊃ nbnba . Як відомо, A має похідні операції 21,..., −nGG , такі, що ISSN 1028-9763. Математичні машини і системи, 2003, № 2 172 ( ) )((( ( ) ) )1,0,11maxmin: −+−−= nianaGi , де 21 −≤≤ ni і Aba ∈, . Легко побачити, що { }21,..., −=ℑ nGG – визначник рівності для M. Таким чином, скінченнозначні логіки Лукасевича охоплюються нашим підходом. Це також стосується логік Поста та інших фунціонально повних логік. (Нагадаємо, що n- значну логіку Поста (так як і будь-яку іншу функціонально повну n-значну логіку) можна отримати з n-значної логіки Лукасевича додаванням до L деяких зв’язок.) 3. Процедури виведення у численнях, що розглядаються Зафіксуємо скінченну пропозиційну мову L, скінченнозначну L-логіку M, визначник рівності ℑ , що складається виключно з головних зв’язок, для M і секвенціальну ( )L,ℑ -таблицю ( )ρλ,=T для M. Проблему існування виведення фіксованої секвенції в численні ( )TMC , можна звести до проблеми суперечності певної скінченної універсальної Хорновської теорії, яка, у свою чергу, має розв’язок. При цьому процедуру розв’язання другої проблеми (яка фактично є детермінованою процедурою оберненого виведення в численні ( )TMC , можна реалізувати в системах декларативного програмування, таких, як АПС [1, 2] або Пролог. Слід відзначити, що інтерактивний інтелектуальний прувер, реалізований у АПС, узагальнює пошук виведення у логічному програмуванні. Тому заради стислості викладення достатньо вивчити питання реалізації процедури оберненого виведення в численні ( )TMC , лише для Пролога. Відзначимо, що пропозиційні змінні інтерпретуються функціональними константами. Таким чином, пропозиційні формули інтерпретуються основними термами (нагадаємо, що пропозиційні зв’язки – це функціональні символи). Інтерпретуючи скінченні множини списками, ми, таким чином, інтерпретуємо ліві і праві частини секвенцій списками основних термів. Для інтерпретації секвенцій ми використуємо тетрарний предикатний символ seq. Інтуїтивно, якщо Г і ∆ – списки формул та Θ і Ξ – списки літер, то вираз ( )Ξ∆Θ ,,,Гseq ототожнюється з секвенцією Ξ∪∆→Θ∪Г . Ми також використовуємо вбудований у Пролог бінарний предикат member. (Нагадаємо, що ( )Гmember ,ϕ означає, що ϕ є елементом списку Г ). Зараз ми покажемо, як, виходячи з логіки M і секвенціальної таблиці T, можна побудувати Пролог- програму ( )ТМР , , яка завершується на запитах, що інтерпретують секвенції, і є такою, що довільна секвенція має виведення в ( )TMC , т.т.т.к., відповідний запит отримує позитивну відповідь в ( )ТМР , . Визначення 3. Пролог-програма ( )ТМР , складається з такої послідовності правил: 1) для кожного 0≥n і кожної n-арної ℑ∈ /Lµ такі два правила: ( )[ ]( ) [ ][ ]({ [ ][ ],\|/,...,1/,,\|/,...,1/:,,,\|,...,1 11 YPnpPpWXPnpPpseqZYWXPnPseq nn ΞΘ−µ ) ( ) }}.\| µλ∈Ξ→ΘZ [ ] ( )[ ]( ) [ ]({ [ ][ ] ) \|,\|/,...,1/,,/,...,1/:,\|,...,1,, 11 ZYPnpPpWPnpPpseqZYPnPWseq nn ΞΘ−µ ( ) }}.µρ∈Ξ→Θ 2) для кожного 0≥n , кожної n-арної L∈µ і кожної ℑ∈v такі два правила: ( ( ) )[ ]( ) [ ][ ]({ [ [ /,...1/,,\|/,...,1/:,,,\|,...,1 11 nn pPpWXPnpPpseqZYWXPnPvseq ΞΘ−µ ] ( ) }}.,\|,\| vZYPn µλ∈Ξ→Θ ( ( ) )[ ]( ) [ ]({ [ ][ ],\|/,...,1/,,/,...,1/:,\|,...,1,[], 11 YPnpPpWPnpPpseqZYPnPvWseq nn ΞΘ−µ ISSN 1028-9763. Математичні машини і системи, 2003, № 2 173 ) ( ) }}.,\| vZ µρ∈Ξ→Θ 3) [ ]( ) [ ]( ).,,\|,:,,,\| ZYWLXseqZYWXLseq − [ ]( ) [ ]( ).\|,,[],:,\|,[], ZLYWseqZYLWseq − 4) для кожної { }0p -літерної секвенції Ξ→Θ , що загальнозначима в M, таке правило: ( ) [ ] )({ } [ ]( ){ }.\|,/,\|,/:[],,[], 00 Ξ∈Θ∈− ψψϕϕ YppmemberXPpmemberYXseq (Порядок речень у програмі може відрізнятися від зазначеного вище. Однак групи речень 1) і 2) мають передувати реченням 3).) Теорема 3. Секвенція ∆→Г має виведення в ( )TMC , т.т.т.к., запит ( )[],[],, ∆Гseq отримує позитивну відповідь в ( )ТМР , . При цьому процедура відповіді на зазначений запит, яка реалізується інтерпретатором Пролога, завершується. Доведення: Відзначимо, що усі (головні та проміжні) запити, що містять предикат seq, є основними. Далі у запитах, що містять предикат member, другий терм є основним. Тому при уніфікації перевірка на уходження змінної не потрібна. (Нагадаємо, що у Пролозі використовується спрощений алгоритм уніфікації, без перевірки на уходження змінної.) Тоді, використовуючи наслідок 3 (оборотність правил) і конструктивне доведення теореми 2, неважко перевірити твердження теореми 3.  Як приклад, розглянемо програму, що відповідає численню Генцена LK [4, 5] щодо класичної логіки, де conj – кон’юнкція, disj – диз’юнкція, impl – імплікація та neg – заперечення: ( )[ ]( ) [ ]( ).,,,\|2,1:,,,\|2,1 ZYWXPPseqZYWXPPconjseq − ( )[ ]( ) [ ]( ) [ ]( ).,,,\|2,,,,\|1:,,,\|2,1 ZYWXPseqZYWXPseqZYWXPPdisjseq − ( )[ ]( ) [ ]( ) [ ]( ).,,,\|2,,\|1,,:,,,\|2,1 ZYWXPseqZYPWXseqZYWXPPimplseq − ( )[ ]( ) [ ]( ).,\|1,,:,,,\|1 ZYPWXsegZYWXPnegseq [ ]( ) [ ]( ).,,\|,:,,,\| ZYWLXseqZYWXLseq − ( )[ ]( ) [ ]( ) [ ]( ).,\|2,[],,,\|1,[],:,\|2,1,[], ZYPWZYPWseqZYPPconjWseq − ( )[ ]( ) [ ]( ).,\|2,1,[],:,\|2,1,[], ZYPPWseqZYPPdisjWseq − ( )[ ]( ) [ ] [ ]( ).,\|2,,1:,\|2,1,[], ZYPWPseqZYPPimplWseq − ( )[ ]( ) [ ]( ).,,,1:,\|1,[], ZYWPseqZYPnegWseq − [ ]( ) [ ]( ).\|,,[],:,\|,[], ZLYWseqZYLWseq − ( ) ( ) ( ).,,,:[],,[], YPmemberXPmemberYXseq − Аналогічні програми побудовані для числень, що уведені у роботах [9, 10, 11, 12]. Висновки Таким чином, доведено, що можна побудувати секвенціальні числення без структурних правил (але з допустимими структурними правилами) для довільних пропозиційних скінченнозначних логік з визначником рівності. Оскільки зазначені числення можна інтерпретувати точними універсальними Хорновськими теоріями та процедура цілеспрямованого виведення для даних теорій, що реалізована в таких системах програмування, як АПС або Пролог, імітує процедуру оберненого виведення в зазначених численнях, можна говорити про ISSN 1028-9763. Математичні машини і системи, 2003, № 2 174 реалізацію логічної задачі пошуку виведення в численнях, побудованих для скінченнозначних логік з визначником рівності, засобами АПС та Пролога. СПИСОК ЛІТЕРАТУРИ 1. Kapitonova J.V., Letichevsky A.A., Konozenko S.V. Computations in aps // Theoretical Computer Science. – 1993. – Vol. 119. – P. 145 –171. 2. Капитонова Ю.В., Летичевский А.А. Об обработке математических текстов в системе алгебраического программирования // Штучний інтелект. – 2000. – Т. 3. – С. 459 – 465. 3. Belnap N.D. A useful four-valued logic // Modern uses of multiple-valued logic. – Dordrecht: D. Reidel Publishing Company, 1977. – P. 8 – 37. 4. Gentzen G. Untersuchungen über das logische Schlißeen (I) // Mathematische Zeitschrift. – 1934. –- Vol. 39. – P. 176 –210. 5. Gentzen G. Untersuchungen über das logische Schließen (II) // Mathematische Zeitschrift. – 1934. – Vol. 39. – P. 405 – 431. 6. Schröter K. Methoden zur Axiomatisierung beliebiger Aussagen- und Prädikatenkalküle // Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. – 1955. – Vol. 1. – P. 214 – 251. 7. Rousseau G. Sequents in many-valued logic (I) // Fundamenta Mathematicae. – 1967. – Vol. 60. – P. 171 – 181. 8. Baaz M., Fermüller C.G., Salzer G. Automated deduction for many-valued logics // Handbook of Automated Reasoning. – Amsterdam: Elsevier Science Publishers, 2001. – P. 1356 – 1402. 9. Попов В.М. Секвенциальные формулировки паранепротиворечивых логических систем // Синтаксические и семантические исследования неэкстенсиональных логик. – М.: Наука, 1989. – С. 285 – 289. 10. Пынько А.П. Структурный семантический подход к построению пропозициональных логических систем: Препр. / Российская АН. Ин-т космических исследований; Пр-1815. – М.: 1992. – 33 с. 11. Pynko A.P. Characterizing Belnap’s logic via De Morgan’s laws // Mathematical Logic Quarterly. – 1995. – Vol. 41, № 2. – P. 442 – 454. 12. Pynko A.P. Functional completeness and axiomatizability within Belnap’s four-valued logic and its expansions // Journal of Applied Non-Classical Logics. –1999. – Vol. 9, N. 1. – P. 61 –105. 13. Общая алгебра: В 2 т. – М.: Наука, 1991. – Т. 2. – 480 с. 14. Los J., Suszko R. Remarks on sentential logics // Ruch Filozoficzny. – 1958. – Vol. 5. – P. 177 – 183. 15. Zygmunt J. Entailment relations on logical matrices (I) // Bulletin of the Section of Logi. – 1979. – Vol. 8. –- P. 112 – 115. 16. Gödel K. Zum intuitionistischen Aussagenkalkül // Anz. Akad. Wiss. Wien. – 1932. – Vol. 69. – P. 65 – 66.

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

Репозитарії

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