Конструктивний алгоритм зворотного методу для числення висловлювань
Розглядається загальна схема зворотного методу С.Ю. Маслова для числення висловлювань. Описано низку евристичних стратегій і правил виведення скорочення перебору. Сформульовано конструктивний алгоритм зворотного методу для числення висловлювань. A general scheme of the inverse method by S. Maslov fo...
Saved in:
| Date: | 2007 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Навчально-науковий комплекс "Інститут прикладного системного аналізу" НТУУ "КПІ" МОН та НАН України
2007
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/14635 |
| 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: | Конструктивний алгоритм зворотного методу для числення висловлювань/ В.А. Доценко // Систем. дослідж. та інформ. технології. — 2007. — № 2. — С. 59-73. — Бібліогр.: 7 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859888622270939136 |
|---|---|
| author | Доценко, В.А. |
| author_facet | Доценко, В.А. |
| citation_txt | Конструктивний алгоритм зворотного методу для числення висловлювань/ В.А. Доценко // Систем. дослідж. та інформ. технології. — 2007. — № 2. — С. 59-73. — Бібліогр.: 7 назв. — укр. |
| collection | DSpace DC |
| description | Розглядається загальна схема зворотного методу С.Ю. Маслова для числення висловлювань. Описано низку евристичних стратегій і правил виведення скорочення перебору. Сформульовано конструктивний алгоритм зворотного методу для числення висловлювань.
A general scheme of the inverse method by S. Maslov for the sentential calculus is considered. A line of heuristic strategies and rules of conclusion on reduction of search and a constructive algorithm for the inverse method for the sentential calculus are described.
Рассматривается общая схема обратного метода С.Ю. Маслова для исчисления высказываний. Описан ряд эвристических стратегий и правил вывода по сокращению перебора. Сформулирован конструктивный алгоритм обратного метода для исчисления высказываний.
|
| first_indexed | 2025-12-07T15:53:49Z |
| format | Article |
| fulltext |
В.А. Доценко, 2007
Системні дослідження та інформаційні технології, 2007, № 2 59
УДК 681:519.68
КОНСТРУКТИВНИЙ АЛГОРИТМ ЗВОРОТНОГО МЕТОДУ
ДЛЯ ЧИСЛЕННЯ ВИСЛОВЛЮВАНЬ
В.А. ДОЦЕНКО
Розглядається загальна схема зворотного методу С.Ю. Маслова для числення
висловлювань. Описано низку евристичних стратегій і правил виведення ско-
рочення перебору. Сформульовано конструктивний алгоритм зворотного ме-
тоду для числення висловлювань.
Одним із завдань теорії штучного інтелекту як важливого напрямку кіберне-
тики є автоматизація процесів доведення, а саме побудова алгоритмів деду-
ктивного виведення теорем. Таке завдання може бути поставлене, зокрема,
для побудови і перевірки доведення існуючих та нововиведених математич-
них теорем, для процесів верифікації даних у базах знань експертних сис-
тем.
Відомо чимало різноманітних алгоритмів автоматичного доведення те-
орем, кожен з яких має сильні та слабкі сторони. Існують певні обмеження
на формат і структуру вхідних даних та форму подання вихідних результа-
тів, тому для вирішення певних завдань необхідно (доцільніше) використо-
вувати одні алгоритми, а для інших — інші. Через це є відкритим питання
створення нових чи розвиток існуючих алгоритмів, які могли би бути ефек-
тивними та зручними. Одним із алгоритмів, що має значний потенціал для
подальших вдосконалень, є зворотний метод С.Ю. Маслова [1,2].
До теперішнього часу існує низка формалізацій зворотного методу, фо-
рмулювання якого для класичного числення предикатів здійснено С.Ю. Ма-
словим [1, 2] і наведено А. Воронковим та А. Дегтярьовим [3], Т. Тамметом
[4], Ф. Пфеннінгом [5]. Формулювання зворотного методу для інтуїтионіс-
тичної та інших некласичних логік здійснене А. Воронковим, Г. Мінцем,
В. Ліфшицом, К. Доннеллі, К. Чаудурі, Ф. Баадером та С. Тобіесом,
А. Бірштунасом та С. Норгелою; для числення предикатів з рівністю
А. Воронковим та А. Дегтярьовим; для числення висловлювань, а також де-
які доповнення навів С.Л. Катречко [6, 7]. Проте всі ці праці об’єднує одна
спільна риса — для зворотного методу наводиться загальна схема без наве-
дення чіткого алгоритму виведення.
Таким чином, існує необхідність побудови конструктивного алгоритму
зворотного методу, який би містив усі необхідні правила оптимізації виве-
дення і мав формулювання для тих логік, для яких існує формулювання за-
гальної схеми зворотного методу.
Ця робота присвячена опису загальної схеми зворотного методу для
числення висловлювань та формулюванню для нього конструктивного алго-
ритму зворотного методу, який може бути безпосередньо застосований для
кодування однією із мов програмування.
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 60
Відповідно до викладення зворотного методу С.Ю. Масловим [1–3],
сформулюємо його схему для числення висловлювань.
Розглянемо дедуктивну систему — секвенційний варіант числення ви-
словлювань. Позначимо його C . Алфавіт числення C складається зі знаків
)(,,,,,, ⋅⇒∀∃∨∧¬ і нескінченного списку ...,, 21 AA , який будемо нази-
вати списком атомів.
Визначення формули будуємо за індукцією:
1. Будь-який атом є формулою.
2. Якщо 1F і 2F — формули, то і 1F¬ , )( 21 FF ∧ , )( 21 FF ∨ формули.
3. Нехай нижче iΓ — позначення списків формул (можливо, порож-
ніх). Секвенцією називається вираз 21 Γ⇒Γ . У нашому випадку приймаємо,
що список формул 1Γ є порожнім.
Приклад 1. ,,, CBA — атоми. Вони також є і формулами. Розглянемо
секвенційне числення висловлювань, де як об’єкти виступають секвенції
вигляду Γ⇒ , де Γ — список формул. Наприклад,
CBCABA ¬¬∧¬∧⇒ ,,, .
• Пропозиційною літерою називається атом або його заперечення.
• Нехай F — деяка формула, що може складатися з однієї пропози-
ційної літери.
• Аксіомами числення C назвемо секвенції вигляду FF ¬⇒ , . Тобто
аксіомою є секвенція, в якій праворуч від знаку секвенції знаходиться тав-
тологія. Аксіому FF ¬, позначимо також як ℵ . Під цим символом будемо
розуміти будь-яку окремо взяту аксіому з числа аксіом числення C (без
конкретизації, яку саме).
• Правила виводу числення C :
a) )(
,,
,,,
2211
2211 ∨⇒
Γ∨Γ⇒
ΓΓ⇒
FF
FF (вставка диз’юнкції);
б) ;)(
,,
,,;,,
2211
221211 ∧⇒
Γ∧Γ⇒
ΓΓ⇒ΓΓ⇒
FF
FF (вставка кон’юнкції);
в) )(
,,,
,,
2211
211 Ι⇒
ΓΓ⇒
ΓΓ⇒
FF
F (вставка формули праворуч від знаку секве-
нції).
Правила виводу застосовуються зверху вниз. У правилі «вставка
диз’юнкції» коми праворуч від знаку секвенції замінюються знаками
диз’юнкції. У правилі «вставка кон’юнкції» відбувається об’єднання двох
секвенцій в одну з утворенням кон’юнкції. У правилі «вставка формули
праворуч від знаку секвенції» до списку формул додається ще одна форму-
ла, що не призводить до втрати виводимості, а лише додає надлишковість.
• Виведенням секвенції F⇒ у численні C назвемо дерево, отримане
застосуванням правил виводу, у вершинах якого знаходяться аксіоми, а в
корені дерева — секвенція F⇒ .
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 61
Дерево будується зверху вниз від аксіом до секвенції, яка виводиться.
Сформулюємо зворотний метод для виведення секвенції F⇒ у чис-
ленні C
δ
1=
=
i
iCF , (1)
де iC — кон’юнктивні формули, що виступають як аргументи диз’юнкції у
формулі F .
Приклад 2. Для секвенції F⇒ , де ∨¬∨∧¬∨∧∧= CBACBAF
DCB ∨¬∧¬∨ , CBAC ∧∧=1 , ,2 BAC ∧¬= CC ¬=3 , CBC ¬∧¬=4 ,
DC =5 . Тут DCBA ,,, — атоми.
Формула F за структурою представлена у диз’юнктивній нормальній
формі.
Нехай iC має вигляд
r
k k
iiiii
i
kkr
DDDDC
1 1
1
= =
==∧∧=
δ
, (1’)
де r є кількістю пропозиційних літер
kiD , з яких складається кон’юнктивна
формула iC . Таким чином, r є функцією від i , адже, у загальному випадку
вона є різною для різних i . Це демонструє інший варіант запису цього чис-
ла — iδ , який показує зв’язок δ , iδ та i . Проте, для простоти запису писа-
тимемо
riD замість
)(iriD чи
iiD
δ
.
Приклад 3. Для прикладу 2 матимемо 5=δ , загалом 31 =δ , 22 =δ ,
13 =δ , 24 =δ , 15 =δ ,
,
321 1111 DDDC ∧∧= де AD =
11 , BD =
21 , CD =
31 , 31 =δ ,
,
21 222 DDC ∧= де AD ¬=
12 , BD =
22 , 22 =δ ,
,
033 DC = де CD ¬=
03 , 13 =δ ,
,
21 444 DDC ∧= де CD ¬=
14 , 2, 442
=¬= δCD ,
,
055 DC = де 0, 550
== δDD .
Третій аргумент диз’юнкції складається з одного атома, тому він (атом)
позначений індексом 0, що підкреслює його єдиність. Такий запис, на пер-
ший погляд, протирічить запису
(1’), проте в цьому є своя доцільність і своє
пояснення. У ході застосування алгоритму зворотного методу за правилом Б
(про це буде розказано далі) необхідно постійно слідкувати за значенням
числа iδ для поточного номера з індексом, щоб залучати до об’єднання
сприятливі набори, які містять повну множину відповідно до поточного но-
мера. При цьому, якщо поточний номер має індекс 0, то немає потреби про-
водити пошук (дивитися значення числа iδ та аналізувати поточну множину
сприятливих наборів), адже 0 одразу вказує: такий індекс є єдиним для да-
ного номера (тобто відповідає аргументу диз’юнкції
0ii DC = ).
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 62
Таким чином, вираз (1’) слід читати так: виконується для всіх 1iδ > ,
для випадку 1iδ = буде виконуватись
0ii DC = .
• h-членним F-набором (h,F-набором) назвемо вираз вигляду
];;[ 1 hii
];;[ 1 hii , (2)
де δ≤≤ hii ,,1 1 , 0≥h .
Такий вираз представляє собою послідовність номерів літер
sjD з jC ,
об’єднаних між собою у набір і приведених до спільної нумерації
( },,1{ δ∈j , },,0{ js δ∈ ).
Зауважимо, що Fh, -набір є лише відображенням літер
sjD на номери
з індексами, а, отже, Fh, -набором ми можемо називати як послідовність
номерів з індексами, записаними у формі (2), так і еквівалентний по суті за-
пис, де замість номерів з індексами будуть стояти самі літери з формули F .
Приклад 4. Покажемо на прикладі, що означає запис (2). Нехай маємо
літери CBA ¬,, , які відповідають
021 321 ,, DDD з формули F , і об’єднані у
3-членний F-набір. Тоді такий 3-членний F -набір можна записати як у ви-
гляді ];;[
021 321 DDD (для нашого прикладу це буде вираз ],,[ CBA ¬ ), так і у
вигляді ]3;2;1[ 021 (у такому записі ми будемо представляти Fh, -набори при
наведенні прикладів застосування алгоритму зворотного методу). Разом з
тим, вираз ];;[
021 321 DDD можемо записати і іншим чином. Введемо нове
допоміжне позначення
0,,1, ≥≤≤= sjiDH
sji δ .
Тобто iH є позначенням з іншим індексом літери
sjD (ця операція ек-
вівалентна перейменуванню та зміні положення аргументів диз’юнкції у
диз’юнктивній формулі F ).
Запишемо наведений вище 3-членний F-набір, застосувавши наше поз-
начення. Отримаємо вираз ];;[ 321 HHH , де
111 DH = ,
221 DH = ,
033 DH = .
Разом з тим, можемо записати і вираз ];;[ 935 HHH , якщо приймемо позна-
чення
115 DH = ,
223 DH = ,
039 DH = за умови 9≥δ . Таке позначення також
буде цілком допустимим. Тому для запису у загальному вигляді нашого
набору через позначення ми повинні записати ];;[
321 iii HHH , де
δ≤≤ 321 ,,1 iii . Якщо запишемо цей набір у еквівалентному вигляді, то ма-
тимемо вираз 321 ;; iii . Нескладно переконатися, що таким чином ми отри-
мали запис нашого 3-членного F -набору у вигляді (2).
• Набором із залежністю є набір, праворуч від якого в дужках запи-
сана деяка (можливо порожня) множина номерів.
)](;;[ 1 Mii h , (2ʹ)
де δ≤≤ hii ,,1 1 , 0≥h , },,2,1{ δ∈M , 0|| ≥M
0|| ≥M
.
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 63
Цьому наборові із залежністю відповідає формула ∨∨∨
321 iii HHH
985 CCC ∨∨∨ .
Приклад 5. Нехай маємо формулу F з прикладу 4, яка має вигляд
(1), і 9≥δ . Нехай набором є ]3;2;1[ 021 . Набором із залежністю буде ви-
раз ]3;2;1[ 021 )9,8,5( .
Для розуміння правил, наведених нижче, варто мати на увазі інтерпре-
тацію Fh, -набору (2) як формули
FHH
hii ′∨∨∨
1
, (3)
де F ′ — формула, яка є диз’юнкцією підмножини (можливо, порожньої)
аргументів диз’юнкту F . Тобто Fh, -набір є представленням диз’юнкції h
пропозиційних літер (у (3) це
hii HH ,,
1
), що входять у склад
кон’юнктивних формул iC . Залежність M є представленням формули F ′
(як було зазначено, вона може бути рівною порожньому диз’юнкту γ ) у ви-
гляді послідовності номерів кон’юнктивних формул δ≤≤ jC j 1, .
Приклад 6. Розглянемо набір із залежністю з прикладу 5: ]3;2;1[ 021
)9,8,5( . Йому відповідає, згідно виразу (3), запис
),,](;;[ 985321
CCCHHH iii ,
де
21 1DHi = ;
22 2DHi = ;
03 3DHi = ; 985 ,, CCC — аргументи диз’юнкції F .
},,{ 985 CCCM = .
• Числення inv
FC ,ℜ називається численням сприятливих наборів, якщо
воно визначається двома правилами — правилом А і правилом Б. Правила
наведемо нижче.
• Об’єктами, що виводяться у численні inv
FC ,ℜ , будуть диз’юнкти ви-
гляду
hii HHT ∨∨=
1
, (4)
де ( 0≥h , δ≤≤ hii ,,1 1 ).
Таким чином, з урахуванням (4) вираз (3) набуває вигляду (позначимо
його FT ′ , де в одному позначенні суміщені позначення сприятливого набо-
ру як T , та залежності M як F ′ ).
FTT F ′∨=′ . (5)
Зокрема, при T γ= (де γ — порожній диз’юнкт) буде =′∨=′ FT F γ
F
= , де F
�
— формула, що є іншим позначенням формули F ′ , яка знахо-
диться у корені дерева виведення, і може бути як рівною F , так і більш
строгою. FT F′ =
�
, коли T γ= і FT ′ =ℵ , де ℵ —одна з аксіом числення
inv
FC ,ℜ , коли F γ′ = .
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 64
Запис (5) показує, які об’єкти знаходяться на кожному кроці дерева ви-
ведення формули при застосуванні зворотного методу. На вершинах цього
дерева (від яких будується виведення) знаходяться аксіоми, а в його корені
(у випадку, коли формула, що виводиться, є загальнозначущою) —
формула F .
Приклад 7. Наведемо схематичний приклад дерева виведення, застосо-
вуючи узагальнені позначення.
Прокоментуємо наведений запис. На листках дерева знаходяться аксіо-
ми ℵ (в цьому випадку ℵ=′FT ). У самому дереві виведення знаходяться
об’єкти, які виводяться, FHH ii ′∨∨
21
(
21 ii HHT ∨= ) та ∨∨
21 jj HH
FH j ′∨∨
3
(
321 jjj HHHT ∨∨= ). Слід зауважити, що F ′ у обох цих
об’єктах є різними — «нижня» F ′ є підмножиною «верхньої» F ′ . Що саме
за цим стоїть, буде видно з прикладу, наведеного наприкінці статті. Окрім
того, звернемо увагу на навмисне застосування нами різних індексів i та j ,
аби не склалося хибного враження, що в обох цих об’єктах, які виводяться
під H , розуміються однакові літери формули F (адже у загальному випад-
ку це не так). У корені дерева бачимо FFFT F
=∨=′∨=′ γγ . Навмисно
перепозначимо F ′ на F
в корені дерева виведення, підкреслюючи, що під
F
ми розуміємо таке F ′ , яке знаходиться в корені дерева виведення.
Аксіоми числення inv
FC ,ℜ задаються наведеним нижче правилом А, а
правило Б — це єдине правило виводу.
• Виведенням секвенції F⇒ у численні inv
FC ,ℜ будемо називати дере-
во, на вершині якого знаходяться аксіоми числення inv
FC ,ℜ (сприятливі набо-
ри), отримані шляхом застосування правила А до секвенції F⇒ . У його
корені знаходиться порожній сприятливий набір, і воно побудоване шляхом
застосування до даних аксіом правила Б.
Правило А. Нехай нам дана деяка секвенція, що має вигляд (1). Якщо
ij ss DD ∨ — тавтологія, то ];[ ij ss є сприятливим набором.
Правило Б. Якщо набори ];[,],;[ 11 rii iHiH
r
сприятливі, то набір
],,[
1 rii HH є сприятливим, де ir δ≡ — кількість підформул формули
i
C
( δ≤≤ rii ,...,1 1 0r ≥ ),
i
C — деяка кон’юнктивна формула.
1ℵ 2ℵ
1 2i iH H F ′∨ ∨ 3ℵ
1 2 3j j jH H H F ′∨ ∨ ∨ 4ℵ
Fγ ∨
�
.
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 65
Зауваження 1. Не слід розуміти під правилом Б таке застосування на-
веденої схеми до сприятливих наборів, коли в результаті виводу буде отри-
мано повну множину індексів більш ніж по одному числу.
Продемонструємо це зауваження на прикладі.
Приклад 8. Нехай початкова формула має вигляд
BABAF ¬∧¬∨∧= .
Як видно, ця формула не є загальнозначущою. Початкова множина
сприятливих наборів (МСН) матиме вигляд }21,21{ 2211 .
Якщо застосувати правило Б так, як забороняє зауваження, то буде по-
будоване таке дерево виведення (для прикладу ми навмисне розіб’ємо одну
операцію на три кроки):
Таким чином, ми вивели загальнозначущість незагальнозначущої фор-
мули.
Тепер пояснимо, що таке розуміння правила Б є хибним. Застосування
правила Б у численні inv
FC ,ℜ відповідає одиничному застосуванню правила
виведення «вставка кон’юнкції» у численні C . Проте у нашому прикладі це
порушується. Покажемо це (перетворимо наведене вище дерево виведення у
численні inv
FC ,ℜ у дерево виведення у численні С).
Як бачимо на детально розписаній гілці, спершу відбувається застосу-
вання правила виведення «вставка кон’юнкції», проте далі йде абсолютно
недопустиме перетворення.
Зауваження 2. Надалі під застосуванням правила Б будемо розуміти
такий його механізм, за яким номер об’єднання наборів переноситься у за-
лежність
1121 1222 1121 1222
□(1,2) => 11122122
2122(1)
□(1,2).
A A∨¬ B B∨¬ A A∨¬ B B∨¬
( )A B A Bγ ∨ ∧ ∨¬ ∧¬ A B A B∧ ∨¬ ∨¬
( )A B A B¬ ∨¬ ∨ ∧
( )A B A Bγ ∨ ∧ ∨¬ ∧¬ .
];[,],;[ 11 rii iHiH
r
...
1
[ , , ] ( )
ri iH H i� .
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 66
Пояснимо тепер детальніше механізм роботи зворотного методу та суть
застосованих нами позначень.
Спершу відбувається побудова множини сприятливих наборів за пра-
вилом А. Для цього аналізується структура формули F , і з її пропозиційних
літер будується ця множина. Такі літери позначаються
kiH (це узагальнене
позначення пропозиційної літери
sjD на даному кроці побудови дерева ви-
ведення). В цілому,
sk ji DH = , },,1,0{ ik δ∈ , },,1,0{ js δ∈ , },,1{, δ∈ji .
F-набір ];[ ki iH
k
необхідно читати так: існує в F таке
sjD
sjD
, що
sjD і
kiD утворюють тавтологію.
У процесі виведення маємо на кожному кроці абсолютно істинні фор-
мули — F-набори ( FT ′ ), що в остаточному результаті у позитивному випад-
ку зводяться до формули F . І навпаки — F-набори визначають зовнішній
вигляд формул, які могли б зустрітися у дереві виведення секвенції F⇒ .
Дерево виведення складається з F-наборів ( FT ′ ), на вершинах якого знахо-
дяться аксіоми ℵ числення inv
FC ,ℜ , а в корені — секвенція F
⇒ . Шукана
секвенція F⇒ отримується із секвенції F
⇒ застосуванням правила
( )⇒ Ι , де як формула 2F , що вставляється, може виступати порожній
диз’юнкт γ .
Приклад 9. Розглянемо приклад застосування правила А та Б. Нехай
маємо початкову формулу з прикладу 2. Сформуємо три перші сприятливі
набори. Ними будуть ]3;1[],4;1[],2;1[ 031211 . Як видно, набори формують
номери з індексами, літери яких формують тавтології. Цих наборів достат-
ньо для того, щоб ми могли один раз застосувати правило Б. Вони містять
повний набір номерів з індексами по номеру 1. Застосуємо правило Б.
За цими позначеннями стоять секвенції, в яких записані формули, абсо-
лютно істинні у численні С. Одні тому, що є його аксіомами, а інші — виво-
димими з аксіом за правилами виводу цього числення.
Як видно з цього прикладу, застосуванням правила Б ми отримали
перший аргумент диз’юнкції початкової формули.
Тепер перейдемо до формулювання конструктивного алгоритму зво-
ротного методу. (Формулювання згадуваного далі правила Б* і доведення
1121 1241 1330
1 2 31 1 2 1 3 1[1 ; ] [1 ; ] [1 ; ]H H H
214130(1)
1 2 31 1 1[ ; ; ] (1)H H H
A A⇒ ∨¬ B B⇒ ∨¬ C C⇒ ∨¬
( )A B C A B C⇒¬ ∨¬ ∨¬ ∨ ∧ ∧ .
.
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 67
правил I–III див. у роботах [6, 7]. Там вони називаються лемами 1...3.) Вва-
жатимемо, що вхідна формула знаходиться у диз’юнктивній нормальній
формі.
При застосуванні правила Б можливе породження значної кількості
сприятливих наборів, які є надлишковими для побудови виводів. Виникає
проблема підвищення ефективності загальної схеми зворотного методу.
Пропонуємо доповнити існуючі евристичні підходи. Введемо ряд необхід-
них означень. Усі ці означення та приведені нижче розміркування наводять-
ся для числення висловлювань.
• Сприятливим набором (СН) називається послідовність чисел з ін-
дексами, де порядок запису цих чисел є несуттєвим. Набір записується в ря-
док без дужок.
• Сприятливим набором із залежністю називається СН, у якому пі-
сля послідовності чисел з індексами в дужках записана послідовність чисел
без індексів.
• Множиною сприятливих наборів (МСН) будемо називати множи-
ну, яка складається з деяких (можливо усіх) СН, що можуть бути побудовані
зі структури початкової формули як за правилом А, так і в результаті засто-
сування правила Б.
• Поточною множиною сприятливих наборів називатимемо таку
МСН, в якій у даний час ведеться пошук СН для застосування правила Б при
побудові дерева виведення. На початку дії алгоритму поточною МСН є по-
чаткова множина СН.
• Гілкою дерева виведення називається послідовність СН, яка побудо-
вана почерговим застосуванням правила Б до СН з поточної МСН.
• Поточною гілкою дерева виведення називається гілка дерева виве-
дення, в якій у даний момент ведеться виведення застосуванням правила Б.
• Поточним сприятливим набором називатимемо СН, що є останнім
(найнижчим) у гілці дерева виводу.
Правило вилучення. При побудові дерева виведення після застосу-
вання правила Б з поточної МСН гілки дерева виведення вилучаються СН,
що брали участь у цьому застосуванні правила Б, а при відкритті нової гілки
дерева виведення поточною МСН є початкова МСН, до якої застосовується
алгоритм прополки і вилучаються усі СН, що містять номери з індексами,
які є поточними в інших гілках дерева виведення.
Доведення. Якщо прослідкувати дерево пошуку виведення прямого
методу, то можна помітити, що розбиття формул на підформули ведеться у
кожній гілці з новими підформулами початкової формули. (Прямий метод
полягає у послідовному розщепленні основної формули на підформули, які
також розщеплюються відповідно до правил секвенційного числення, аж
доки усі гілки дерева не будуть містити тавтології. У випадку, коли цього
досягнуто, таке дерево, що називається деревом пошуку виведення, стає де-
ревом виведення, і загальнозначущість початкової формули вважається до-
веденою. Зворотний метод «перевертає» напрямок побудови дерева виводу,
ведучи його від аксіом-тавтологій і закінчуючи початковою формулою.
Звідси він і отримав свою назву — зворотний метод.) Підформули, за якими
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 68
відбувається розгалуження дерева виведення на гілки, лишаються лише у
власних гілках і не зустрічаються в інших. Таким чином, базуючись на цьо-
му спостереженні, робимо висновок, що при зворотній побудові дерева ви-
ведення як початкові підформули кожної гілки також будуть застосовува-
тись підформули різних формул, тобто різні СН. Тому можемо вилучати СН
одразу після їх використання за правилом Б при побудові кожної гілки дере-
ва виведення.
Примітка. У ряді випадків є можливим здійснення побудови дерева
виведення й тоді, коли поточна МСН нової гілки будується не з початкової
МСН, а з поточної МСН останньої гілки. Таке формулювання правила вилу-
чення будемо називати «сильним», у той час як наведене вище — «слаб-
ким». Застосування «сильного» формулювання правила вилучення може
дати суттєве скорочення виведення. Тому можливо застосування схеми, за
якою побудова дерева виведення здійснюється із застосуванням «сильного»
формулювання правила вилучення, а коли таке виведення не завершується
вдало, то побудова дерева виведення здійснюється із застосуванням «слаб-
кого» правила вилучення, починаючи з тої гілки, виведення якої не може
бути завершене виводом нольчленного СН або СН, який містить тільки двічі
обрамлені номери. (Пояснення того, що собою представляють обрамлені та
двічі обрамлені номери, буде наведене нижче.)
Правило вилучення дає можливість побудувати не лише нові евристики
для зворотного методу, а і змінює умови дії вже існуючих. Наведемо їх з
урахуванням нових означень.
Правило I. Якщо у деякому поточному СН зустрічається число з інде-
ксом таке, що повної сукупності індексів по даному числу у поточній МСН
немає, то усі такі набори без втрати виводимості можна виключити з поточ-
ної МСН, окрім того випадку, коли повна сукупність індексів формується
разом із числами з індексами із СН, поточними в інших гілках дерева виве-
дення.
Доведення. Доведемо не саме правило, а доповнення до нього (обме-
ження дії). Необхідність такого обмеження обумовлюється тим, що за наве-
деним нижче алгоритмом допускається існування декількох гілок дерева
виводу, у поточних сприятливих наборах яких можуть бути числа з індекса-
ми, відсутніми у поточній МСН.
Правило II. Якщо у складі поточної МСН зустрічаються набори, що
містять числа з індексом нуль, то усі такі набори можна викреслити, зміни-
вши індексацію інших чисел цих наборів в решті початкових сприятливих
наборах. Саме число з індексом нуль переноситься у залежність усіх сприя-
тливих наборів поточної МСН.
Доведення. Доведемо не саме правило, а доповнення до нього. Необ-
хідність такого доповнення полягає у необхідності розширення застосуван-
ня зворотного методу до вироджених випадків. Наприклад, для формули
AA ¬∨ початковою множиною сприятливих наборів буде }21{ 00 . Застосу-
вавши до неї правило II отримаємо множину {□}, що свідчить про вдале за-
вершення зворотного методу. Проте залежність порожня, а отже ми не виве-
ли загальнозначущість початкової формули. Застосовуючи правило у
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 69
новому формулюванні, одержуємо множину {□(1,2)}, тобто вивід загально-
значущості початкової формули.
Правило III. За наявності серед поточної МСН такого СН, який є під-
множиною деякого знову отриманого СН, використання цього нового СН
для отримання виводу є надлишковим.
Правило IV. Якщо у ході виведення було отримано такий СН, що у по-
точній МСН є набори, які є надмножиною цього нового набору, то тоді без
втрати виводимості необхідно вилучити усі такі набори.
Доведення. Дія правила ґрунтується на правилі поглинання і є синте-
зом правил II і III з проекцією на однолітерний СН.
• Алгоритмом прополки поточної МСН називається застосування до
поточної МСН правил I...IV. (Даний термін запозичено з роботи [6] і розши-
рено за змістом на ще одне правило.)
Правило V. Якщо після побудови початкової МСН застосували (мож-
ливо, неодноразово) алгоритм прополки поточної МСН, і в результаті отри-
мали порожній СН, то тоді необхідно вважати отриману в залежності фор-
мулу загальнозначущою.
Доведення. Коректність застосування правила II до початкової МСН
було доведено вище, тому покажемо, що застосування інших правил не за-
важатиме вдалому завершенню виведення без застосування правила Б. Пра-
вило I вилучає набори, застосування яких у побудові дерева виведення при-
зведе то того, що виведення продовжувати далі буде неможливо. Тому
вилучення цих сприятливих наборів не вплине на виведення загальнозначу-
щості початкової формули. Правила III і IV можуть застосовуватись лише
після правила Б, адже у початковій множині СН усі набори однакової дов-
жини. Тому на виводимість вони вплинути не можуть. Отож, правила I, III,
IV на можливість отримання виведення загальнозначущості початкової фо-
рмули до першого застосування правила Б не впливають, а правило II спри-
яє цьому. Лишається довести коректність неодноразового застосування ал-
горитму прополки початкової множини СН. Розглянемо це на прикладі.
Нехай початкова формула буде
CBABCBA ∧∧∨∧¬∨¬∨¬⇒ ,
а початкова множина СН
}43,42,32,41{ 31202010 .
Застосувавши алгоритм прополки перший раз, отримуємо
При цьому в алгоритмі прополки ми застосували правило ІІ.
Слід звернути увагу, що ми змінили індексацію третього і четвертого
елементів диз’юнкції і перенесли у залежність номери з нульовими індекса-
ми у викреслених наборах.
{1041, 2032, 2042, 3040(1,2)}.
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 70
Оскільки у поточній МСН є номери з нульовими індексами, то знову
застосовуємо алгоритм прополки (правило ІІ). Отримуємо
Правило VI. Якщо у застосуванні правила Б при побудові поточної гі-
лки дерева виведення повний набір індексів за поточним номером можливий
лише при такому залученні сприятливих наборів, коли у результаті застосу-
вання до них правила Б буде отримано повний набір індексів більш ніж по
одному номеру, то без втрати виводимості необхідно викреслити з поточної
МСН усі СН з поточним номером.
Доведення. Правило VI вказує на дії, які потрібно виконати у випадку,
коли при виборі СН можна залучити лише СН, що призведе до отримання
повного набору індексів більш ніж по одному номеру. Такий результат про-
тирічить правилу виводу ( ∧⇒ ), на якому базується правило Б. Тому вилу-
чення таких СН не вплине на виводимість початкової формули.
Додаткові правила до загальної схеми зворотного методу. Окрім до-
поміжних у виводі правил, сформулюємо декілька правил для ефективної
побудови дерева виведення.
1. Правило обрамлення. При виводі СН номер, що переходить у зале-
жність, обрамлюється.
2. Правило пріоритету. Розглядати номери у СН для встановлення по-
точності та при підборі СН з поточної МСН слід згідно із їх пріоритетом:
обрамленість, кількість індексів у поточному СН, номер. У обрамленості по
залученню СН пріоритет мають двічі обрамлені, потім необрамлені, обрам-
лені номери; встановлені поточності — необрамлені, потім обрамлені, двічі
обрамлені; у кількості індексів у поточному СН більший пріоритет мають
номери, у яких їх більше. Згідно із номерами більший пріоритет мають ме-
нші номери.
3. Правило скорочення. Якщо у поточному СН є два чи більше номерів
з однаковими індексами, то слід їх скоротити до одного.
4. Правило вітвлення. Якщо поточний СН складається з одного номе-
ра, то проводиться аналіз початкової МСН (при застосуванні «слабкого»
правила вилучення) чи поточної МСН (при «сильному» правилі). Якщо є
більше одного СН, що містить доповнюючі номери з індексами до поточно-
го СН поточної гілки, то тоді відкривається нова гілка, інакше у поточній
гілці виведення продовжується. Застосовувати правило Б до однолітерних
СН можна, лише коли по усім гілкам дерева виведення поточні СН склада-
ють повний набір індексів.
5. Правило подвійного обрамлення. При відкритті нової гілки поточ-
ний номер поточного СН двічі обрамлюється.
6. Правило об’єднання двічі обрамлених номерів. Правило Б застосо-
вується до двічі обрамлених номерів з індексами тоді і тільки тоді, коли во-
ни є поточними у гілках дерева виведення і формують повний набір індексів
за номером.
{□(1,2,3,4)}. {3040(1,2)}, тобто
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 71
Конструктивний алгоритм зворотного методу. Тепер сформулюємо
схему алгоритму, який конструктивно визначить послідовність дій зворот-
ного методу виведення загальнозначущості формули. Для спрощення ідею
методу проілюструємо на численні висловлювань.
1. Привести початкову секвенцію ∆⇒Γ (де Γ і ∆ — можливо, поро-
жні списки формул) до вигляду F⇒
F⇒
, де F знаходиться у КНФ.
2. Формуємо початкову МСН за правилом А.
3. Застосовуємо алгоритм прополки поточної МСН (можливо, неодно-
разово).
4. Якщо поточна МСН порожня (містить порожній СН), то переходимо
на крок 5, інакше крок 6.
5. Якщо у порожнього СН в залежності є номери, то переходимо на
крок 10, інакше крок 8.
6. Дивимося, чи можна застосувати правило Б*. Якщо так, то йдемо на
крок 7. Якщо ні, то крок 8.
7. Застосовуємо почергово правило Б* і правило вилучення з алго-
ритмом прополки доти, доки для застосування правила Б* не буде необ-
хідних СН, або коли буде виведено порожній СН. Якщо у ході виводу
жодного разу не застосовувалося правило Б, то переходимо на крок 9,
інакше крок 10. При застосуванні правила Б* необхідно дотримуватися
правил 1...6 та VI.
8. Початкова формула не є загальнозначущою. Переходимо на 11.
9. Початкова формула є суперечливою. Переходимо на 11.
10. Початкова формула є загальнозначущою. Переходимо на 11.
11. Кінець алгоритму.
Приклад застосування конструктивного алгоритму зворотного ме-
тоду. Нехай дано формулу
∨∨∨¬∨¬⇒ DCDCADCDA &&&&&
DAADBDACB ¬¬∨¬¬∨¬¬∨ &&&&&& .
Використовуючи правило А, отримуємо початкову множину СН
,62,52,52,42,32,41,31,21,71,61,51{ 2242211121223222113131
}74,64,54,73,63,53,73,63,53,72 22224213234311313122 .
Застосовуємо алгоритм прополки. Виявили відсутність зібрання індек-
сів за номерами 5 та 6. За правилом І вилучаємо усі СН, які містять ці номе-
ри. Поточна МСН
}74,73,73,72,42,32,41,31,21,71{ 22131122112122322211 .
Застосовуємо алгоритм прополки. Поточна МСН коректна. Розпочина-
ємо виведення.
В.А. Доценко
ISSN 1681–6048 System Research & Information Technologies, 2007, № 2 72
1 Вибір СН і поточного номера з індексом здійснено за правилом пріоритету.
2 При виводі буде повне зібрання індексів по 3 і 7. Застосовуємо правило VI.
3 Гілка продовжується за правилом вітвлення.
4 Номер обрамлено за правилом обрамлення.
5 Номер двічі обрамлено за правилом подвійного обрамлення.
6 Розпочинається нова гілка за правилом вітвлення.
Згідно із конструктивним формулюванням правила вилучення поточна МСН
нової гілки буде такою:
}74,72,42,42,41,31{ 222211112232 .
Застосовуємо алгоритм прополки. Немає повного зібрання індексів за
номерами 1 і 3. Вилучаємо СН, які містять ці номери. Поточна МСН має ви-
гляд }74,72,42,42{ 22221111 .
Застосовуємо алгоритм прополки. Поточна МСН коректна. Розпочина-
ємо виведення.
7 Поточна МСН: {∅}.
8 За правилом об’єднання двічі обрамлених номерів проводимо об’єднання
першої та другої гілок.
Виведення завершено виводом формули 7,4,3,2,1⇒ , тобто F ′⇒ , що є
більш конструктивною за F .
2) 22[[72]] 2141
41[[72]](2) 42[[72]]
[[72]](2,4)7 [[71]]8(1,2,3,7)
□ (1,2,3,4,7)
1) 1171
1 1222
2271(1) 2132
3271(1,2)2 3171 3372
3271(1,2) 3372
3233(1,2,7)3 31[71]4
[[71]]5(1,2,3,7)6
Конструктивний алгоритм зворотного методу для числення висловлювань
Системні дослідження та інформаційні технології, 2007, № 2 73
ВИСНОВКИ
Конструктивний алгоритм зворотного методу полягає у постановці чітких
правил, при дотриманні яких процес виведення буде коротким та однознач-
ним. Подальший розвиток алгоритму полягає у його формулюванні для усіх
числень, для яких існує формулювання загальної схеми зворотного методу,
та у пошуку оптимізаційних правил, що враховують специфіку цих числень
для забезпечення здійснення мінімального виведення.
ЛІТЕРАТУРА
1. Маслов С.Ю. Обратный метод установления выводимости для логических
исчислений // Тр. матем. ин-та им. В.А. Стеклова АН СССР. — 98. — М.:
Ин-т им. В.А. Стеклова АН СССР. — 1968. — С. 26–87.
2. Маслов С.Ю. Теория дедуктивних систем и ее применения. — М.: Радио и
связь, 1986. — С. 90–114.
3. Degtyarev A., Voronkov A. The inverse Method, in A. Robinson & A. Voronkov,
eds, `Handbook of Automated Reasoning. — 2001. — P. 181–270.
4. Tammet T. Resolution, inverse method and the sequent calculus. In A. Leitsch
G. Gottlog and D. Mundici, editors, Proceedings of the 5th Kurt Godel Col-
loquium on Computational Logic and Proof Theory (KGC'97). — Vienna:
Springer-Verlag LNCS, 1997. — P. 65–83.
5. Pfenning F. Automated theorem proving. — Pittsburgh PA: Carnegie Mellon Uni-
versity, 2004. — P. 93–116.
6. Катречко С.Л. Модификации обратного метода С.Ю. Маслова // Материалы X
Всесоюзн. конф. по логике, методологии и философии науки. — М.: ИФ
РАН, 1990. — С. 7–18.
7. Катречко С.Л. Моделирование правила расщепления в обратном методе
С.Ю. Маслова // Логические методы в компьютерных науках. — М.: ИФ
РАН, 1991.— С. 24–36.
Надійшла 05.04.2006
Конструктивний алгоритм зворотного методу для числення висловлювань
В.А. Доценко
ВИСНОВКИ
|
| id | nasplib_isofts_kiev_ua-123456789-14635 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1681–6048 |
| language | Ukrainian |
| last_indexed | 2025-12-07T15:53:49Z |
| publishDate | 2007 |
| publisher | Навчально-науковий комплекс "Інститут прикладного системного аналізу" НТУУ "КПІ" МОН та НАН України |
| record_format | dspace |
| spelling | Доценко, В.А. 2010-12-27T13:50:09Z 2010-12-27T13:50:09Z 2007 Конструктивний алгоритм зворотного методу для числення висловлювань/ В.А. Доценко // Систем. дослідж. та інформ. технології. — 2007. — № 2. — С. 59-73. — Бібліогр.: 7 назв. — укр. 1681–6048 https://nasplib.isofts.kiev.ua/handle/123456789/14635 681:519.68 Розглядається загальна схема зворотного методу С.Ю. Маслова для числення висловлювань. Описано низку евристичних стратегій і правил виведення скорочення перебору. Сформульовано конструктивний алгоритм зворотного методу для числення висловлювань. A general scheme of the inverse method by S. Maslov for the sentential calculus is considered. A line of heuristic strategies and rules of conclusion on reduction of search and a constructive algorithm for the inverse method for the sentential calculus are described. Рассматривается общая схема обратного метода С.Ю. Маслова для исчисления высказываний. Описан ряд эвристических стратегий и правил вывода по сокращению перебора. Сформулирован конструктивный алгоритм обратного метода для исчисления высказываний. uk Навчально-науковий комплекс "Інститут прикладного системного аналізу" НТУУ "КПІ" МОН та НАН України Проблемно і функціонально орієнтовані комп’ютерні системи та мережі Конструктивний алгоритм зворотного методу для числення висловлювань Constructive algorithm for inverse method of sentential calculus Конструктивный алгоритм обратного метода для исчисления высказываний Article published earlier |
| spellingShingle | Конструктивний алгоритм зворотного методу для числення висловлювань Доценко, В.А. Проблемно і функціонально орієнтовані комп’ютерні системи та мережі |
| title | Конструктивний алгоритм зворотного методу для числення висловлювань |
| title_alt | Constructive algorithm for inverse method of sentential calculus Конструктивный алгоритм обратного метода для исчисления высказываний |
| title_full | Конструктивний алгоритм зворотного методу для числення висловлювань |
| title_fullStr | Конструктивний алгоритм зворотного методу для числення висловлювань |
| title_full_unstemmed | Конструктивний алгоритм зворотного методу для числення висловлювань |
| title_short | Конструктивний алгоритм зворотного методу для числення висловлювань |
| title_sort | конструктивний алгоритм зворотного методу для числення висловлювань |
| topic | Проблемно і функціонально орієнтовані комп’ютерні системи та мережі |
| topic_facet | Проблемно і функціонально орієнтовані комп’ютерні системи та мережі |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/14635 |
| work_keys_str_mv | AT docenkova konstruktivniialgoritmzvorotnogometodudlâčislennâvislovlûvanʹ AT docenkova constructivealgorithmforinversemethodofsententialcalculus AT docenkova konstruktivnyialgoritmobratnogometodadlâisčisleniâvyskazyvanii |