Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів
Досліджені області застосування конструктивного алгоритму зворотного методу, здійснена оцінка
 доцільності застосування конструктивного алгоритму зворотного методу, виходячи з поставлених
 задач. Проведена оцінка складності побудови початкової множини сприятливих наборів. Розглянуто&...
Saved in:
| Date: | 2008 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут проблем штучного інтелекту МОН України та НАН України
2008
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/7136 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів / В.А. Доценко // Штучний інтелект. — 2008. — № 3. — С. 655-662. — Бібліогр.: 11 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860076530313461760 |
|---|---|
| author | Доценко, В.А. |
| author_facet | Доценко, В.А. |
| citation_txt | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів / В.А. Доценко // Штучний інтелект. — 2008. — № 3. — С. 655-662. — Бібліогр.: 11 назв. — укр. |
| collection | DSpace DC |
| description | Досліджені області застосування конструктивного алгоритму зворотного методу, здійснена оцінка
доцільності застосування конструктивного алгоритму зворотного методу, виходячи з поставлених
задач. Проведена оцінка складності побудови початкової множини сприятливих наборів. Розглянуто
приклади застосування конструктивного алгоритму зворотного методу для секвенцій різного вигляду,
а також випадку, коли застосування конструктивного алгоритму зворотного методу не є ефективним.
Исследована область применения конструктивного алгоритма обратного метода исходя из поставленных
задач. Проведена оценка сложности построения начального множества благоприятных наборов.
Рассмотрены примеры применения конструктивного алгоритма обратного метода для секвенций
различного вида, а также случая, когда применение конструктивного алгоритма обратного метода не
является эффективным.
|
| first_indexed | 2025-12-07T17:13:59Z |
| format | Article |
| fulltext |
«Штучний інтелект» 3’2008 655
8Д
УДК 681:519.68
В.А. Доценко
Національний технічний університет України «Київський політехнічний інститут»
validator1982@mail.ru
Особливості застосування конструктивного
алгоритму зворотного методу
для секвенційного числення предикатів
Досліджені області застосування конструктивного алгоритму зворотного методу, здійснена оцінка
доцільності застосування конструктивного алгоритму зворотного методу, виходячи з поставлених
задач. Проведена оцінка складності побудови початкової множини сприятливих наборів. Розглянуто
приклади застосування конструктивного алгоритму зворотного методу для секвенцій різного вигляду,
а також випадку, коли застосування конструктивного алгоритму зворотного методу не є ефективним.
Вступ
Конструктивний алгоритм зворотного методу (КАЗМ) був нами розглянутий
у працях [1-3]. Він є розширенням зворотного методу (ЗМ) С.Ю. Маслова [4] за
рахунок вдосконалення його та застосування евристик із упорядкування виведення
та зі скорочення перебору.
Перш ніж застосовувати конструктивний алгоритм зворотного методу для
пошуку виведення, слід знайти відповіді на наступні питання:
1. Якою є предметна область застосування КАЗМ?
2. Яка область доцільності застосування КАЗМ?
3. Як можна оцінити складність КАЗМ?
4. Чи можливі випадки неефективної роботи КАЗМ?
Під першим питанням ми розуміємо числення, для яких може бути застосо-
ваний КАЗМ. Під другим питанням ми розуміємо задачі та формат вхідних формул,
для вирішення яких доцільно застосовувати КАЗМ. Під третім питанням ми розу-
міємо потребу здійснення оцінки як кількості кроків на застосування алгоритму, так
і для порівняльного аналізу складності застосування алгоритму для різних вхідних
формул. Під четвертим питанням ми розуміємо пошук випадків, для яких процес
виведення за КАЗМ потребує істотно більшої кількості кроків, ніж для іншого ва-
ріанта застосування КАЗМ. Якщо такі випадки можливі, необхідно визначити шляхи
щодо мінімізації появи таких випадків.
В даній статті ми дамо відповіді на поставлені питання, а також наведемо
приклади роботи КАЗМ у секвенційному численні предикатів першого порядку.
Область застосування КАЗМ
Конструктивний алгоритм зворотного методу є об’єднанням методів скоро-
чення перебору та упорядкування процесу виведення при застосуванні зворотного
методу. Нами було доведено, що їх застосування не призводить до втрати методом
виводимості. Тому область застосування КАЗМ збігається з такою для ЗМ. На даний
момент існують формулювання ЗМ для логіки висловлювань [5], теорії предикатів
Доценко В.А.
«Искусственный интеллект» 3’2008 656
8Д
першого порядку з рівністю [6] та без [7], для модальної логіки S4 [8], для лінійної
логіки [9]. Щодо інших логічних числень, які не були нами перелічені, то для них
застосування ЗМ (а отже, і КАЗМ) можливе – для цього потрібно лише провести
аналіз допустимості та здійснити формулювання методу з урахуванням синтаксису
та семантики даного числення. На даний момент нами було сформульовано КАЗМ
для логіки висловлювань та для логіки предикатів першого порядку без рівності.
Відмінністю КАЗМ для різних числень є входження до КАЗМ евристичних доповнень,
що враховують специфіку конкретного числення, а отже, можуть бути застосовані
лише на ньому.
Формат вхідних формул, з якими працює КАЗМ, є ширшим від такого для
методу резолюцій. Якщо розглядати секвенційне числення предикатів першого
порядку, то КАЗМ здатен опрацьовувати формули вигляду:
Γ ⇒ ∆ , (1)
де
1
( )( )
n
i
i
x A
=
Γ = ∀ ∩ , 0n > , – список змінних,
1
i
si i
s
A A
δ
=
=∪ , 0iδ ≥ ,
1
( )( )
m
j
j
y B
=
∆ = ∃ ∪ ,
0m > , – список змінних,
1
j
kj j
k
B B
δ
=
=∩ , 0jδ ≥ ,
lpA , uB
ν
– відкриті формули, що
можуть складатися з одної літери. Графічно рівні літери скорочені до однієї.
Тут ,Γ ∆ знаходяться у зведеній нормальній формі.
Також КАЗМ опрацьовує формули вигляду ⇒ ∆ (2) та Γ⇒ (3).
КАЗМ будує дерево виведення без початкового перенесення усіх підформул до
антицидента чи до сукцидента.
Область доцільності застосування КАЗМ
Ми приведемо ключові переваги КАЗМ та окреслимо задачі, для яких ці
переваги є ключовими при виборі алгоритму пошуку виведення. Порівнюватимемо
КАЗМ з методом резолюції. Випишемо переваги кожного із цих методів у порів-
нянні їх між собою.
Переваги КАЗМ:
− вхідна формула може бути представлена секвенціями вигляду (1-3);
− вхідну формулу не є необхідним перетворювати до ССФ, достатньо перетворити
її до зведеної нормальної форми;
− дерево виведення може бути просто трансльоване на природну мову, кожен з
вузлів дерева є аксіомою числення, в якому здійснюється виведення;
− відсутня необхідність перетворення вхідної формули до вигляду (3), де формула
представлена у ССФ.
Переваги методу резолюції:
− відсутня трудомістка процедура побудови початкової множини сприятливих наборів;
− наявні для модифікацій методу резолюцій евристики є більш простими за такі у
КАЗМ (а отже, потребують меншої кількості операцій);
− відсутня необхідність повторної побудови дерева виведення з початку, у випадку
невірного вибору поточного сприятливого набору.
Виходячи з приведеної інформації, ми вважаємо, що для узагальненого
випадку, коли стоїть лише задача встановлення виводимості формули, а вхідні
формули представлені у вигляді (3) або ж відносно просто до нього перетворюються,
доцільнішим є застосовувати метод резолюції. Якщо перетворення формул до того
вигляду, у якому їх здатен обробляти метод резолюції, є трудомістким, то визна-
Особливості застосування конструктивного алгоритму зворотного методу…
«Штучний інтелект» 3’2008 657
8Д
чення кращого з цих двох методів не є однозначним. Якщо є потреба у трансляції
кожного вузла дерева виведення на природну мову (така необхідність є в експертних
системах для перевірки експертом ходу розмірковування або видачі його користу-
вачу), то слід застосовувати зворотний метод.
Оцінка складності КАЗМ
Перш за все відмітимо, що КАЗМ відноситься до методів повного перебору, а
отже, має експоненційну складність. Щодо можливої оцінки (порівняльної оцінки)
його складності, то КАЗМ має свої особливості, які безпосередньо впливають на
його складність.
У кожного методу є свої переваги і недоліки, при цьому, як правило, недоліки є
продовженням переваг. Це стосується і зворотного методу. Основною його ідеєю є
побудова дерева виводу з аксіом (сприятливих наборів), що будуються зі структури
формули, яку необхідно довести. Проте це породжує проблему – побудованих
сприятливих наборів (СН) значно більше, ніж це є необхідно для побудови дерева
виведення. Для того, щоб зменшити навантаження на алгоритм, у попередніх працях
нами було приведено ряд евристик та допоміжних правил, направлених на
скорочення потужності множини сприятливих наборів.
Ми здійснимо оцінку потужності множини початкових сприятливих наборів.
Така оцінка буде проводитись виходячи зі структури формули, яку нам необхідно
довести. Отримана формула й буде орієнтовною оцінкою складності методу,
оскільки вивести узагальнену формулу розрахунку кількості кроків, які витрачає
алгоритм на виведення формули, не є можливим – в залежності від вхідної формули,
від шляху, за яким піде алгоритм, кількість кроків алгоритму може бути істотно
різною, і здійснити попередньо таку оцінку для КАЗМ не є можливим. Щодо оцінки
кількості сприятливих наборів у початковій множині сприятливих наборів, то від
них в першу чергу залежить величина дерева виведення – чим більша кількість
сприятливих наборів, тим більшим буде дерево пошуку виведення. Другим
фактором є непередбачувана специфіка кожної вхідної формули.
Отож здійснимо оцінку потужності початкової множини сприятливих наборів.
Кількістю додатних літер атому a ми будемо називати число літер цього
атому, що входять у початкову формулу без заперечення. Це число позначатимемо an+ .
Кількістю від’ємних літер атому a ми будемо називати число літер цього
атому, що входять у початкову формулу із запереченням. Це число позначатимемо an− .
Кількістю комбінацій атому a ми будемо називати добуток кількості додатних
літер атому a і кількості від’ємних літер атому a. Це число позначатимемо aκ .
Тепер ми можемо сформулювати нашу оцінку:
Нехай F – формула, в якій графічно рівні літери скорочені до однієї. Тоді кіль-
кість сприятливих наборів, що можуть бути побудовані з цієї формули, складатиме
1
,
p
i
i
κ
=
Κ =∑
(4)
де p – кількість атомів формули .F
Приклад 1. Нехай початковою формулою буде
F A B C A B C A B C D B D D= ∧ ∧ ∨ ¬ ∧ ∧ ∨ ∧¬ ∨ ¬ ∧ ∨ ¬ ∧ ∨ ¬ .
Тоді 2An+ = , 1An− = , 2Aκ = , 2Bn+ = , 2Bn− = , 4Bκ = ,
2Cn+ = , 1Cn− = , 2Cκ = , 2Dn+ = , 1Dn− = , 2Dκ = .
Доценко В.А.
«Искусственный интеллект» 3’2008 658
8Д
Застосовуючи формулу (4), маємо: 2 4 2 2 10Κ = + + + = .
Побудуємо початкову множину сприятливих наборів для F :
1 1 2 2 2 1 3 1 1 1 2 2 2 2 3 1 2 0 2 01 2 , 1 3 , 1 5 , 1 4 , 2 3 , 2 3 , 2 5 , 2 4 , 4 6 , 5 6 .
Як бачимо, кількість початкових сприятливих наборів становить 10, що збіг-
лося з нашою оцінкою.
Приклади застосування КАЗМ для секвенційного
числення предикатів першого порядку
Розглянемо тепер декілька прикладів застосування КАЗМ пошуку виведення
вхідної формули у численні предикатів першого порядку, які демонструють най-
більш характерні особливості побудови ним дерева виведення. Перші два приклади
показують застосування роботу КАЗМ у секвенційному численні предикатів пер-
шого порядку для вхідних формул, представлених у вигляді секвенцій різного виду,
третій приклад демонструє випадок неефективної роботи КАЗМ, коли під час побудови
гілки дерева виведення доводиться повертатись до самого початку, вибирати поточ-
ним інший номер з індексом і заново будувати дерево виведення.
Розглянемо спершу приклад, який показує застосування КАЗМ для вхідної
формули, представленої у вигляді (2).
Приклад 2. Нехай маємо секвенцію вигляду
( ( , ) ( ( )) ( ( ), ( ))) ( ( , ( )) ( ) ( ( ), ( ))).x y P x y R f x P f x f y x y P x f x R y P f x f x⇒∃ ∃ ∧ ∨¬ ∨∃ ∃ ¬ ∧¬ ∧
Застосуємо до неї описаний нами вище алгоритм. Маємо
1. Перейменування змінних:
1 2 1 2 1 1 2( ( , ) ( ( )) ( ( ), ( )))x x P x x R f x P f x f x⇒∃ ∃ ∧ ∨¬ ∨
3 4 3 4 4 3 3( ( , ( )) ( ) ( ( ), ( )))x x P x f x R x P f x f x∨∃ ∃ ¬ ∧¬ ∧ .
2. Внесення мета змінних:
∨¬∨∧⇒ }/,/{*))(),((}/{*))((}/,/{*),( 221121111221121 xtxttftfPxttfRxtxtttP
}/{*))(),((}/{*)(}/{*))(,( 33334442343 xttftfPxttRxttftP ∧¬∧¬∨ .
3. Побудова початкової МСН:
{ })],/,/{)),(,((});/,/)(,/,/{)),(,([( 3335552225111555 xttttftPxtttfxttttftP ¬
})],/,/)({)),(((});/,/{)),(([( 4446611166 xtttftfRxttttfR ¬
})]/,/{)),(),(((});/,/,/,/{)),(),(([( 3337772227111777 xttttftfPxtttxttttftfP¬ }.
В номерах ця МСН має вигляд:
)]},3();,2[()],,3();,1[()],,3();,1{[( 635042322111 ξξξξξξ ,
де iξ , 6,,1…=i – відповідні F-підстановки.
4. Побудова дерева виведення
4.1. }/{ 581 tt=σ , }/{ 682 tt=σ , }/,/,/,/,/)(,/,/{ 11166822151558 xtttttxtttftttt=σ
1131 2231
2133 (1)
Поточний СН має вигляд:
})]/,/)(,/{)),(((});/,/,/{)),(,([( 444668833355888 xtttftttfRxttttttftP ¬¬ .
4.2. }/{ 891 tt=σ , }/{ 792 tt=σ ,
}/,/,/,/,/)(,/,/,/,/,/{ 33377944466833355889 xtttttxtttfttxttttttt=σ .
Особливості застосування конструктивного алгоритму зворотного методу…
«Штучний інтелект» 3’2008 659
8Д
4.3. }/,/,/,/,/{ 2227111779 xtttxttttt=σ
3032 )1(33 21
)3,1(20
)3,2,1(γ
Тут γ – символ порожнього сприятливого набору.
5. Виведення завершене виводом секвенції:
∨∧⇒ }/,/,/,/,/)(,/,/,/{*))(())(,( 1116682225111558888 xtttttxtttfxttttttfRtftP
∨¬∨ }/,/,/,/,/{*))(),(( 222711177999 xtttxttttttftfP
}/,/,/,/)(,/,/{*)))(),(())(())(,(( 33794446688999999 xtttxtttftttttftfPtfRtftP ∧¬∧¬∨ .
Якщо ми спростимо підстановки, то отримаємо:
∨∧⇒ }/)(,/{*))(())(,( 2818888 xtfxttfRtftP ∨¬ }/,/{*))(),(( 271999 xtxttftfP
}/,/)({*)))(),(())(())(,(( 394999999 xtxtftftfPtfRtftP ∧¬∧¬∨ .
Ми встановили виводимість початкової секвенції.
Розглянемо тепер приклад встановлення виводимості αβ -секвенції (1).
Приклад 3. Нехай маємо секвенцію вигляду
( ( , ) ( ( )) ( ( ), ( ))) ( ( , ( )) ( ) ( ( ), ( ))).x y P x y R f x P f x f y x y P x f x R y P f x f x∀ ∀ ¬ ∨¬ ∧ ⇒∃ ∃ ¬ ∧¬ ∧
Застосовуємо алгоритм.
1. Перейменування змінних:
1 2 1 2 1 1 2( ( , ) ( ( )) ( ( ), ( )))x x P x x R f x P f x f x∀ ∀ ¬ ∨¬ ∧ ⇒
3 4 3 3 4 3 3( ( , ( )) ( ) ( ( ), ( )))x x P x f x R x P f x f x⇒∃ ∃ ¬ ∧¬ ∧ .
2. Внесення мета змінних:
⇒∧¬∨¬ }/,/{*))(),((})/{*))((}/,/{*),(( 221121111221121 xtxttftfPxttfRxtxtttP
}/{*))(),((}/{*)(}/{*))(,( 33334442343 xttftfPxttRxttftP ∧¬∧¬∨ .
3. Побудова початкової МСН:
{ ],})/,/{)),(,((;})/,/)(,/,/{)),(,([( 3335552225111555
βα xttttftPxtttfxttttftP ¬¬
],})/,/)({)),(((;})/,/{)),(([( 4446611166
βα xtttftfRxttttfR ¬¬
]})/,/{)),(),(((;})/,/,/,/{)),(),(([( 3337772227111777
βα xttttftfPxtttxttttftfP }.
В номерах ця МСН має вигляд: )]},3();,2[()],,3();,1[()],,3();,1{[( 635042322111 ξξξξξξ βαβαβα ,
де iξ , 6,,1…=i – відповідні F-підстановки.
4. Побудова дерева виведення:
})]/,/{,3(});/,/)(,/,/{,1[( 33351222511151 xtttxtttfxttt βα
})]/,/)({,3(});/,/{,1[( 4446211162 xtttfxttt βα
1 8 5 5 3 3 3 2 8 6 6 4 4 4 1[(3 ,{ / , / , / }) ; (3 ,{ / , ( ) / , / }) ] (1 * )t t t t t x t t f t t t xβ β α θ
})]/,/{,3(});/,/,/,/{,2[( 33373222711170 xtttxtttxttt βα
0 7 1 1 1 7 2 2 2 1 3[(2 ,{ / , / , / , / })] (1 * ,3 * )t t t x t t t xα α βθ θ
1 2 3(1 * , 2 * ,3 * )α α βγ θ θ θ
Доценко В.А.
«Искусственный интеллект» 3’2008 660
8Д
де 1 8 5 5 1 5 1 2 2 8 6 6 1 1 1{ / , / , ( ) / , / , / , / , / }t t t t f t t t x t t t t t xθ = , 2 9 7 7 1 1 1 7 2 2 2{ / , / , / , / , / }t t t t t x t t t xθ =
3 9 8 8 6 6 4 4 4 9 7 8 5 7 3 5 3 3 3{ / , / , ( ) / , / , / , / , / , / , / }t t t t f t t t x t t t t t t t t t xθ = .
5. Виведення завершене виводом секвенції (підстановки скоротили):
8 8 8 8 1 5 2 9 9 9 1 9 2( ( , ( )) ( ( ))*{ / , ( ) / }) ( ( ), ( ))*{ / , / }P t f t R f t t x f t x P f t f t t x t x∨¬ ∧¬ ⇒
9 9 9 9 9 9 4 9 3( ( , ( )) ( ( )) ( ( ), ( )))*{ ( ) / , / }P t f t R f t P f t f t f t x t x¬ ∧¬ ∧ .
Приведений приклад демонструє лінійний порядок виведення. Проте не завжди таке
може бути здійснене. Розглянемо приклад, в якому процес виведення є неефективним.
Приклад 4. Розглянемо приклад «цікаве життя», який був запозичений з [11].
Задані твердження:
1. Усі небідні та розумні люди щасливі: ( ( ) ( ) ( ))x poor x smart x happy x∃ ¬ ∧ → .
2. Людина, яка читає книги, розумна: ( ( ) ( ))y read y smart y∀ → .
3. Джон вміє читати і є багатою людиною: ( ) ( )read John poor John∧¬ .
4. Щасливі люди живуть цікавим життям: ( ( ) ( ))z happy z exiting z∀ → .
Необхідно отримати відповідь на питання: Чи існує людина, яка живе цікавим жит-
тям? Питання має вигляд: ( ( ))w exiting w∃ .
Запишемо формулу, яку необхідно вивести для відповіді на поставлене питання.
Вона має вигляд:
( ( ( ) ( ) ( ))) ( ( ( ) ( )))x poor x smart x happy x y read y smart y∃ ¬ ∧ → ∧ ∀ → ∧
( ( ) ( )) ( ( ( ) ( ))) ( ( ))read John poor John z happy z exiting z w exiting w∧¬ ∧ ∀ → ⇒∃ .
Перейменуємо предикати на літери A та B .
11 12 13 21 22 31 32( ( ( ) ( ) ( ))) ( ( ( ) ( ))) ( ( ) ( ))x A x A x A x y A y A y A J A J∃ ¬ ∧ → ∧ ∀ → ∧ ∧¬ ∧
41 42 10( ( ( ) ( ))) ( ( ))z A z A z w B w∀ → ⇒∃ .
Приведемо формулу до зведеної нормальної форми і введемо метазмінні.
1 2 1 2 1 2 1 2( ( ( , )) ( ( , )) ( ( , ))) { ( , ) / }poor f t t smart f t t happy f t t f t t x∨¬ ∨ ∗ ∧
1 1 1( ( ) ( ))*{ / }read t smart t t y¬ ∨ ∧
2 2 2 3 3( ( ) ( )) ( ( ) ( ))*{ / } ( )*{ / }read J poor J happy t exiting t t z exiting t t w∧¬ ∧ ¬ ∨ ⇒ .
Перейдемо до позначення предикатів номерами і сформуємо початкову множину сприят-
ливих наборів. Для зручності при кожному номері будемо писати два індекси – перший
індекс буде позначати номер літери в підформулі, другий індекс (через знак «/») позна-
чатиме кількість літер у даній підформулі. Таким чином, не буде потреби дивитись на
початкову формулу, щоб дізнатись кількість літер у підформулі.
1/3 1 2 1 2 2/2[(1 ,{ / ( , ), ( , ) / }) ; (3 ,{ }) ]J f t t f t t x α α∅ ,
2/3 4 1 5 2 1 2 2/2 4 5 1 1[(1 ,{ / , / , ( , ) / }) ; (2 ,{ ( , ) / , / }) ]t t t t f t t x f t t t t yα β
3/3 6 1 7 2 1 2 1/2 6 7 2 2[(1 ,{ / , / , ( , ) / }) ; (4 ,{ ( , ) / , / }) ]t t t t f t t x f t t t t zα α
1/2 1 1 1/2[(2 ,{ / , / }) ; (3 ,{ }) ]J t t y α α∅ , 2/2 7 2 2 0 7 3 3[(4 ,{ / , / }) ; (5 ,{ / , / }) ]t t t z t t t wα β .
Застосовуючи алгоритм прополки, переносимо число 5 в залежність п’ятого сприят-
ливого набору. Вибираємо згідно з правилом пріоритету поточний сприятливий набір та
починаємо будувати дерево виведення.
1 2 1 2 2/21/3[( ,{ / ( , ), ( , ) / }) ; (3 ,{ }) ]1 J f t t f t t x α α∅
2/3 4 1 5 2 1 2 2/2 4 5 1 1[(1 ,{ / , / , ( , ) / }) ; (2 ,{ ( , ) / , / }) ]t t t t f t t x f t t t t yα β
3/3 6 1 7 2 1 2 1/2 6 7 2 2[(1 ,{ / , / , ( , ) / }) ; (4 ,{ ( , ) / , / }) ]t t t t f t t x f t t t t zα α
2/2 2/2 4 5 4 5 1 1 1/2 6 7 6 7 2 2[(3 ,{ }) ; (2 ,{ / ( , ), ( , ) / , / }) ; (4 ,{ / ( , ), ( , ) / , / }) ](1 )J f t t f t t t t y J f t t f t t t t zα α α α∅
Особливості застосування конструктивного алгоритму зворотного методу…
«Штучний інтелект» 3’2008 661
8Д
Подальша побудова дерева виведення блокується за правилом VI – поточна
множина сприятливих наборів містить лише такі СН, застосування до яких правила
Б призведе до отримання повного набору індексів більш ніж по одному номеру. Для
продовження виведення необхідно повернутись до початкової множини сприятливих
наборів і розпочати гілку дерева виведення з іншого номеру. При цьому помітимо
номер 1 як такий, пошук номерів з індексами по якому слід вести в останню чергу.
1 1 1/21/2[( ,{ / , / }) ;(3 ,{ }) ]2 J t t y α α∅
2/3 4 1 5 2 1 2 2/2 4 5 1 11[( ,{ / , / , ( , ) / }) ; (2 ,{ ( , ) / , / }) ]t t t t f t t x f t t t t yα β
1/3 1 2 1 2 2/2[(1 ,{ / ( , ), ( , ) / }) ; (3 ,{ }) ]J f t t f t t x α α∅
3/3 6 1 7 2 1 2 1/2 6 7 2 2[(1 ,{ / , / , ( , ) / }) ; (4 ,{ ( , ) / , / }) ]t t t t f t t x f t t t t zα α
2/2 7 2 2 5[(4 ,{ / , / }) ](5 * )t t t z α β θ
2/3 4 5 4 1 5 2 1 2 11/21[( ,{ / ( , ), / , / , ( , ) / }) ;( ,{ }) ](2 * )3J f t t t t t t f t t x α α α θ∅
2/3 4 5 4 1 5 2 1 2 1/3 1 2 1 2 1 2[(1 ,{ / ( , ), / , / , ( , ) / }) ;(1 ,{ / ( , ), ( , ) / }) ](2 * ,3 * )J f t t t t t t f t t x J f t t f t t xα α α αθ θ
1/2 6 7 6 7 2 2 1 2 3[(4 ,{ / ( , ), ( , ) / , / }) ](1 * , 2 * ,3 * )J f t t f t t t t z α α α αθ θ θ
1 2 3 4 5(1 * ,2 * ,3 * , 4 * ,5 * )α α α α βγ θ θ θ θ θ
де 1 1 2 4 5 4 1 5 2 6 7 6 1 7 2 1 2{ / ( , ), / ( , ), / , / , / ( , ), / , / , ( , ) / }J f t t J f t t t t t t J f t t t t t t f t t xθ = ,
2 1 1 4 1 5 2 1 2{ / , / , / , / , ( , ) / }J t t y t t t t f t t xθ = ,
3 { }θ = ∅ ,
4 6 7 6 7 2 2 7 2 2{ / ( , ), ( , ) / , / , / , / }J f t t f t t t t z t t t zθ = ,
5 1 1 4 1 5 2 1 2{ / , / , / , / , ( , ) / }J t t y t t t t f t t xθ = .
Виведення завершене виводом порожнього сприятливого набору, а отже, по-
чаткова теорема доведена (твердження, що існує людина, яка живе цікавим життям,
виведене).
Як було продемонстровано на наведеному прикладі, при аналізі кількості літер
у підформулах (індексів при номерах) при залученні сприятливих наборів для засто-
сування правила Б слід віддавати перевагу в першу чергу тим номерам, по яким є
менша кількість індексів (підформулам з меншою кількістю літер). В такому ви-
падку отриманий після застосування правила Б сприятливий набір буде містити
меншу кількість номерів з індексами, а отже, ймовірність появи випадку, коли спра-
цьовує правило VI, буде знижена. При застосуванні такої методики (застосування
приведеного правила до формули з прикладу 2) виведення одразу буде вестись за
другою гілкою.
Доценко В.А.
«Искусственный интеллект» 3’2008 662
8Д
Висновок
КАЗМ може застосовуватись для широкого класу формул, але область доціль-
ності його застосування є меншою. В даній статті вказано задачі, для яких засто-
сування КАЗМ є доцільнішим за застосування методу резолюції. Ми також навели
приклади застосування КАЗМ для виведення формул у секвенційному численні
предикатів першого порядку, показали випадок, коли виведення КАЗМ є неефектив-
ним, та вказали методику для зменшення таких випадків.
Література
1. Доценко В.А. Конструктивний алгоритм зворотного методу для числення висловлювань //
Системні дослідження та інформаційні технології. – 2007. – № 2. – С. 59-73.
2. Доценко В.А. Конструктивний алгоритм зворотного методу для секвенцій загального вигляду //
Искусственный интеллект. – 2006. – № 3. – С. 120-128.
3. Доценко В.А. Конструктивний алгоритм зворотного методу для секвенційного числення
предикатів // Вісник національного технічного університету України «Київський політехнічний
інститут»: інформатика, управління та обчислювальна техніка. – 2007. – № 46. – С. 211-225.
4. Маслов С.Ю. Обратный метод установления выводимости в классическом исчислении предикатов //
ДАН ССР. – 1964. – № 1. – С. 17-20.
5. Катречко С.Л. Модификации обратного метода С.Ю. Маслова // Материалы X Всесоюзной конфе-
ренции по логике, методологии и философии науки. – М., 1990.
6. Voronkov A. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor //
Proceedings of the 11-th International Conference on Automated Deduction, Saratoga Springs. – New York,
1992. Springer-Verlag LNCS 607. – P. 618-662.
7. Degtyarev A., Voronkov A. Equality Elimination for the Inverse Method and Extension Procedures. – Uppsala
(Sweden), 1995.
8. Degtyarev A., Voronkov A. The inverse Method, in A. Robinson & A. Voronkov eds. Handbook of
Automated Reasoning, 2001. – P. 181-270.
9. Chaudhuri K. Theorem Proving with the Inverse Method for Linear Logic. – Pittsburgh PA: Carnegie
Mellon University, 2004.
10. Birstunas A., Norgela S. Inverse method for modal logic S4 // Matemetikos ir informatikos institutas,
T34, 2003.
11. Люгер Д. Искусственный интеллект. – М.: Мир, 2003. – 690 с.
В.А. Доценко
Особенности применения конструктивного алгоритма обратного метода для секвенциального
исчисления предикатов
Исследована область применения конструктивного алгоритма обратного метода исходя из поставленных
задач. Проведена оценка сложности построения начального множества благоприятных наборов.
Рассмотрены примеры применения конструктивного алгоритма обратного метода для секвенций
различного вида, а также случая, когда применение конструктивного алгоритма обратного метода не
является эффективным.
Стаття надійшла до редакції 24.07.2008.
|
| id | nasplib_isofts_kiev_ua-123456789-7136 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1561-5359 |
| language | Ukrainian |
| last_indexed | 2025-12-07T17:13:59Z |
| publishDate | 2008 |
| publisher | Інститут проблем штучного інтелекту МОН України та НАН України |
| record_format | dspace |
| spelling | Доценко, В.А. 2010-03-24T17:41:08Z 2010-03-24T17:41:08Z 2008 Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів / В.А. Доценко // Штучний інтелект. — 2008. — № 3. — С. 655-662. — Бібліогр.: 11 назв. — укр. 1561-5359 https://nasplib.isofts.kiev.ua/handle/123456789/7136 681:519.68 Досліджені області застосування конструктивного алгоритму зворотного методу, здійснена оцінка
 доцільності застосування конструктивного алгоритму зворотного методу, виходячи з поставлених
 задач. Проведена оцінка складності побудови початкової множини сприятливих наборів. Розглянуто
 приклади застосування конструктивного алгоритму зворотного методу для секвенцій різного вигляду,
 а також випадку, коли застосування конструктивного алгоритму зворотного методу не є ефективним. Исследована область применения конструктивного алгоритма обратного метода исходя из поставленных
 задач. Проведена оценка сложности построения начального множества благоприятных наборов.
 Рассмотрены примеры применения конструктивного алгоритма обратного метода для секвенций
 различного вида, а также случая, когда применение конструктивного алгоритма обратного метода не
 является эффективным. uk Інститут проблем штучного інтелекту МОН України та НАН України Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів Особенности применения конструктивного алгоритма обратного метода для секвенциального исчисления предикатов Article published earlier |
| spellingShingle | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів Доценко, В.А. Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем |
| title | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів |
| title_alt | Особенности применения конструктивного алгоритма обратного метода для секвенциального исчисления предикатов |
| title_full | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів |
| title_fullStr | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів |
| title_full_unstemmed | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів |
| title_short | Особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів |
| title_sort | особливості застосування конструктивного алгоритму зворотного методу для секвенційного числення предикатів |
| topic | Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем |
| topic_facet | Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/7136 |
| work_keys_str_mv | AT docenkova osoblivostízastosuvannâkonstruktivnogoalgoritmuzvorotnogometodudlâsekvencíinogočislennâpredikatív AT docenkova osobennostiprimeneniâkonstruktivnogoalgoritmaobratnogometodadlâsekvencialʹnogoisčisleniâpredikatov |