Приклад: Гільбертові системи для двопропозиційних логік

У гільбертовій системі^[en] передумови та висновки правил виведення є просто формулами якоїсь мови, зазвичай із застосуванням метазмінних. Задля графічної компактності та для підкреслення різниці між аксіомами та правилами виведення цей розділ використовує послідовний запис (⊢) замість вертикального представлення правил.

Формальну мову класичної пропозиційної логіки може бути виражено з використанням лише заперечення (), імплікації (→) та пропозиційних символів. Загальновідома аксіоматизація, що включає схему з трьох аксіом та одне правило виведення (modus ponens):

(CA1) ⊢ A → (B → A)
(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))
(CA3) ⊢ (A → B) → (B → A)
(MP) A, A → B ⊢ B

Може здаватися зайвим мати два поняття виведення у цьому випадку, ⊢ та →. У класичній пропозиційній логіці вони дійсно збігаються; теорема дедукції^[en] свідчить, що A ⊢ B тоді й лише тоді, коли ⊢ A → B. Проте навіть у цьому випадку існує варта уваги відмінність: перший запис описує дедукцію, що є діяльністю з переходу від виразів до виразів, тоді як A → B є просто формулою, зробленою із застосуванням логічного сполучника, в даному випадку імплікації. Без правила виведення (як modus ponens у даному випадку) немає дедукції або виведення. Цей момент ілюструється в діалозі Льюїса Керрола «Що Черепаха сказала Ахіллові»^[en].^[3]

Для деяких некласичних логік теорема дедукції не виконується. Наприклад, тризначну логіку Ł3 Лукашевича може бути аксіоматизовано таким чином:^[4]

(CA1) ⊢ A → (B → A)
(LA2) ⊢ (A → B) → ((B → C) → (A → C))
(CA3) ⊢ (A → B) → (B → A)
(LA4) ⊢ ((A → A) → A) → A
(MP) A, A → B ⊢ B

Ця послідовність відрізняється від класичної логіки зміною аксіоми 2 та додаванням аксіоми 4. Класична теорема дедукції для цієї логіки не виконується, проте виконується видозмінена форма, а саме A ⊢ B тоді й лише тоді, коли ⊢ A → (A → B).^[5]

Прийнятність та вивідність

Детальніші відомості з цієї теми Ви можете знайти в статті Правило прийнятності ^[en].

Правило виведення може бути зайвим у наборі правил в тому сенсі, що воно є прийнятним або вивідним. Вивідне правило — це таке правило, чиї висновки може бути виведено з його передумов за допомогою інших правил. Прийнятним є таке правило, чиї висновки виконуються, коли виконуються його передумови. Усі вивідні правила є прийнятними. Щоби оцінити різницю, розгляньмо наступний набір правил для визначення натуральних чисел (судження^[en] стверджує той факт, що є натуральним числом):

Перше правило стверджує, що 0 є натуральним числом, а друге стверджує, що s(n) є натуральним числом, якщо ним є n. У цій системі доведення наступне правило, що демонструє, що другий наступник (англ. successor) натурального числа також є натуральним числом, є вивідним:

Його виведенням є композиція двох застосувань правила наступника, наведеного вище. Наступне правило для ствердження існування попередника будь-якого ненульового числа є лише прийнятним:

Це є дійсним фактом натуральних чисел, оскільки його може бути доведено індукцією. (Щоби довести, що це правило є прийнятним, розгляньте виведення передумови, і зробіть індуктивний перехід за ним, отримавши виведення .) Але воно не є вивідним, оскільки воно залежить від структури виведення передумови. Через це вивідність зберігається при доповненнях системи доведення, тоді як прийнятність — ні. Щоби побачити різницю, припустімо, що до цієї системи доведення було додано наступне безглузде правило:

У цій новій системі правило другого наступника залишається вивідним. Однак правило знаходження попередника більше не є прийнятним, оскільки немає немає способу вивести . Крихкість прийнятності походить від способу її доведення: оскільки доведення може робити індуктивний перехід за структурою виведень передумов, розширення системи додають нових випадків до цього доведення, що можуть вже й не задовольнятися.

Прийнятні правила можна розглядати як теореми системи доведення. Наприклад, у численні секвенцій, в якому виконується усунення перетинів^[en], правило перетину є прийнятним.

Проблема вибору

Проблема вибору має тільки два можливих виходи, так чи ні (або 1 чи 0) для будь-якого входу.

У теорії обчислень і теорії складності обчислень, проблема вибору або задача про приймання рішень це запитання в деякій формальній системі з відповіддю так або ні, залежно від значення деяких вхідних параметрів. Наприклад, «дані два числа x і y, чи ділиться x на y без залишку?» — проблема вибору. Відповідь може бути або 'так' або 'ні', і залежить від значень x і y.

Метод розв'язання проблеми вибору даний у формі алгоритму називається алгоритмом вибору, алгоритмом приймання рішень або розв’язувальною процедурою для цієї проблеми. Розв'язувальна процедура для проблеми вибору «дані два числа x і y, чи x ділиться на y без залишку?" має надати покроковий набір дій для визначення чи ділиться x на y без залишку для даних x і y. Одним з таких алгоритмів є ділення в стовпчик. Якщо залишок нуль, тоді відповідь 'так' інакше 'ні'. Проблема вибору, яка може бути розв'язана за допомогою алгоритму, такого як в цьому прикладі, зветься розв'язною.

Теорія складності обчислень розрізняє розв'язні проблеми вибору за складністю їхнього розв'язання. «Складний», у цьому значені, описаний в термінах обчислювальних ресурсів потрібних найефективнішому алгоритму для певної проблеми. Теорія обчислень, тим часом, розрізняє нерозв'язні проблеми вибору за степенем Тюрінга, який є мірою неров'язності властивої будь-якому розв'язку.

Дослідження в теорії обчислень зазвичай сфокусовані на проблемах вибору, від цього не втрачається загальність, бо кожна функціональна проблема може бути перетворена у проблему вибору.

Алгоритми пошуку рішень

Алгори́тм пошуку́ в глибину́ (англ. Depth-first search, DFS) — алгоритм для обходу графа, робота якого починається з кореня дерева (або іншої обраної вершини в графі) і здійснюється обхід на максимально можливу глибину до переходу на наступну вершину. Порядок обходу вершин наведений на рис.17.5.

Нехай - простий зв'язний граф, усі вершини якого позначено попарно різними символами. У процесі пошуку вглиб вершинам графа G надають номери (DFS -номери, які для вершини х позначають DFS (х)) та зберігають дані, які відповідають вершинам в множині, що називається стеком. Зі стеку можна вилучити тільки той елемент, котрий було додано до нього останнім: стек працює за принципом - "останній прийшов - перший вийшов". Таким чином, додавання й вилучення елементів у стеку відбувається з одного кінця, який називається верхівкою стеку, за наступним алгоритмом:

Крок 1. Почати з довільної вершини v. Виконати DFS (v):=1. Включити вершину v у стек.

Крок 2. Розглянути вершину у верхівці стеку - нехай це вершина х. Якщо всі ребра, інцидентні вершині х, позначено, то перейти до кроку 4, інакше - до кроку 3.

Крок 3. Нехай { x, y } - непозначене ребро. Якщо DFS (у) уже визначено, то позначаємо ребро { x, y } і визначаємо DFS (у) як черговий DFS -номер, включаємо цю вершину в стек і переходимо до кроку 2.

Крок 4. Виключити вершину х зі стеку. Якщо стек порожній, то зупинитись, інакше - перейти до кроку 2.

Обчислювальною складністю алгоритму (або просто складністю) назвемо кількість кроків виконуваних алгоритмом в гіршому випадку. Вона є функцією від розмірності задачі, представленої вхідними даними. Наприклад, для графа, що задається списками інцидентності, розмірність задачі представляється як пара . Складність алгоритму визначається, як функція f, така, що дорівнює кількості кроків алгоритму для довільного графа з n вершинами і m ребрами. Під кроком алгоритму розуміється машинна команда, і при такому визначенні кроку обчислювальна складність залежить від конкретної системи команд і способу трансляції. Нас же буде надалі цікавити не точна складність алгоритму, обчислення якої практично неможливо, а асимптотична складність, яка визначається швидкістю зростання кількості кроків алгоритму при необмеженому збільшенні розмірності задачі. Крім того, обчислювальна складність алгоритму, обчислена при різних системах команд або способах трансляції, відрізняються один від одного в p разів, де p - речова константа, а їх швидкість росту однакова. Для порівняння швидкості росту двох функцій f(n) i g(n) будемо використовувати позначення f(n) = O[g(n)] або f(n) = Ω[g(n)]. Будемо говорити, що функція f(n) має порядок зростання не більше, ніж функція g(n), що позначається f(n) = O[g(n)], тоді і тільки тоді, коли існують C = const і N > 0, такі, що |f(n)| <= C|g(n)| n>= N Будемо говорити, що функція f(n) має порядок зростання не менше, ніж функція g(n), що позначається f(n) = Ω[g(n)], тоді і тільки тоді, коли існують C = const і N > 0, такі, що |f(n)| >= C|g(n)| n>= N Оцінимо обчислювальну складність рекурсивного варіанту алгоритму пошуку у глибину. O(n) + O(2m) = O(n) + O(m) = O(n+m)

По́шук у ширину́ — алгоритм пошуку на графі.^[1]

Якщо задано граф G = (V, E) та початкову вершину s, алгоритм пошуку в ширину систематично обходить всі досяжні із s вершини. На першому кроці вершина s позначається, як пройдена, а в список додаються всі вершини, досяжні з s без відвідування проміжних вершин. На кожному наступному кроці всі поточні вершини списку відмічаються, як пройдені, а новий список формується із вершин, котрі є ще не пройденими сусідами поточних вершин списку. Для реалізації списку вершин найчастіше використовується черга. Виконання алгоритму продовжується до досягнення шуканої вершини або до того часу, коли на певному кроці в список не включається жодна вершина. Другий випадок означає, що всі вершини, доступні з початкової, уже відмічені, як пройдені, а шлях до цільової вершини не знайдений.

Алгоритм має назву пошуку в ширину, оскільки «фронт» пошуку (між пройденими та непройденими вершинами) одноманітно розширюється вздовж всієї своєї ширини. Тобто, алгоритм проходить всі вершини на відстані k перед тим як пройти вершини на відстані k +1.^[1]

Пошук у ширину

Порядок обходу вершин.

 

Наведемо кроки алгоритму

1. Почати з довільної вершини v. Виконати BFS(v):=1. Включити вершину v у чергу.
2. Розглянути вершину, яка перебуває на початку черги; нехай це буде вершина х. Якщо для всіх вершин, суміжних із вершиною х, уже визначено BFS-номери, то перейти до кроку 4, інакше - до кроку 3.
3. Нехай {x,y} - ребро, у якому номер BFS(у) не визначено. Позначити це ребро потовщеною суцільною лінією, визначити BFS(у) як черговий BFS-номер, включити вершину у у чергу й перейти до кроку 2.
4. Виключити вершину х зі черги. Якщо черга порожня, то зупинитись, інакше - перейти до кроку 2.

Двонапра́влений по́шук — ускладнений алгоритм пошуку ушир або пошуку углиб, в основі якого лежить така ідея, що можна одночасно проводити два пошуки (в прямому напрямку, від початкового стану, та у зворотному напрямку, від цілі), зупиняючись після того, як два процеса пошуку зустрінуться на середині (Рис. 1).

Файл:Bidirectional search.PNG

Рис. 1. Схема двонаправленого пошуку. Тут він має успішно завершитися після того, як одна з гілок, що йде з початкового вузла, зустрінеться з гілкою з цільового вузла