Сколемовські стандартні форми обчислення предикатів
Сколемовські стандартні форми обчислення предикатів - розділ Освіта, Основні поняття та визначення Очевидно, Що Якщо Формули F І Ф рівносильні, то F Логічно нездійсненна тоді.
Очевидно, що якщо формули F і Ф рівносильні, то F логічно нездійсненна тоді і тільки тоді, коли логічно нездійсненна Ф. Завдяки цьому твердженню і через те, що алгоритми приведення до ПНФ зберігають рівносильність нездійсненних формул, в подальших процедурах доказу можна обмежитися формулами, мають пренексний вигляд, і навіть ще вужчим класом формул, так званими "-формулами".
Формула F називається "-формулою, якщо вона представлена в ПНФ, причому кванторна частина складається тільки з кванторів загальності, тобто.
F = "x1" x2 … "xr M, де М - безкванторна формула.
Таким чином, виникає завдання усунення кванторів існування у формулах, поданих у ПНФ. Це можна зробити шляхом введеннясколемівських функцій.
Нехай формула представлена в ПНФ і нехай zi (1 i r) - квантор існування в префіксі. Якщо i = 1, т. е. жоден квантор загальності не стоїть перед квантором існування, то вибирається константасз області визначення М, відмінна від констант, що зустрічаються в М, і замінюється х1 насв М. З префіксу квантор існування z1x1 викреслюється. Якщо перед квантором існування zi стоїтьmкванторів загальності, то вибирається m-місцевий функціональний символ f, відмінний від функціональних символів М, і замінюється xi на функцію f(xj1, xj2, … xjm), звану сколемівською функцією . Квантор існування zi xi викреслюється із префікса.
Алгоритм послідовного виключення кванторів існування з ПНФ, заснований на описаній процедурі, називаєтьсяалгоритмСколема :
1. Формулу подати до ПНФ.
2. Знайти найменший індекс i такий, що z1z2 … zi-1 – всі рівні”, але zi = $. Якщо i = 1, то замість х1 у формулу М підставити константус, відмінну від констант, що зустрічаються у М. Якщо такого i немає, то формула F є "-формулою".
3. Взяти новий (i -1)-місцевий функціональний символ fi, що не зустрічається в F, та замінити xi на fi (х1, …, xi-1). Перейти до кроку 2.
Перехід від формули до ПНФ до "-формули не зачіпає властивість формули бути нездійсненною. Таким чином, алгоритм Сколема, зберігаючи властивість нездійсненності, наводить довільну формулу, що має пренексний вигляд, до "-формули.
Безкванторна частина формули (матриця) має бути наведена до КНФ. Алгоритм рівносильного перетворення довільної безкванторної формули КНФ аналогічний алгоритму, викладеному в обчисленні висловлювань.
Отже, послідовним застосуванням алгоритмів приведення до ПНФ, Сколема та приведення до КНФ із збереженням властивості нездійсненності будь-яка формула F може бути представлена набором диз'юнктів, об'єднаних кванторами загальності. Така формула називається формулою,представленою в Сколемівській стандартній формі (ССФ).
Приклад. Навести формулу F до ССФ.
1. F = "x [P(x) Ù "y $ x (¬Q(x, y) U "z R (a, x, y))].
2. "x" y $u [P(x) Ù (Q(u,y) UR (a,u,y))].
4. "x" y [P(x) Ù (Q(f(x,y),y) UR (a, f(x,y),y))]].
Ця тема належить розділу:
Основні поняття та визначення
В даний час штучний інтелект одна з областей науки, що швидко розвиваються, яка розробляє методи і засоби пошуку рішень. Ідея створення штучної подоби людського розуму для вирішення складних.друга розвинули цю ідею запропонувавши.
Що робитимемо з отриманим матеріалом:
Всі теми цього розділу:
Поняття штучного інтелекту Центральним поняттям є поняття «штучний інтелект». Термін штучний інтелект (artificial intelligence) був запропонований у 1956 р. на науковому семінарі у Стендфордсько
Попов Е.В., Фірдман Г.Р. (Алгоритмічні основи інтелектуальних роботів та штучний інтелект, 1992 р.) «Під системою ІІ розуміється система, що володіє здатністю до накопичення та коригування знання на основі активного сприйняття інформації про світ і до цілеспрямованої поведінки на основі накопичень
Цілі та завдання штучного інтелекту До основних цілей штучного інтелекту можна віднести: 1. Обробка зорових сцен: - обробка зображення; - Розпізнавання та розуміння образів; - машинна
Витоки формальних міркувань 2.1. Як відомо, мозок людини складається з двох півкуль, кожна з яких по-своєму перетворює інформацію. Весь навколишній світ ділить
Типи мислення Ліва півкуля – «Я» Тип мислення Подібність – відмінність Виділення ознак конкретних об'єктів Декомпозиція цілого на частини
Розв'язність формальної системи Першим питанням, яке виникає при завданні формальної системи, є питання про інверсію, тобто про те, чи можливо, розглядаючи будь-яку формулу формальної системи, визначити, чи є
Інтерпретація формальної системи Формальні системи є не просто грою розуму, а завжди являють собою модель якоїсь реальності (або конкретної, або математичної). Інтерпретація представл
Доказ і істинність З наведених вище визначень існує вже запобудові глибоке різницю між концепціями докази і істинності. Ці поняття відносяться до двох різних галузей. Апріорно ніщо не гара
Основні принципи силлогістики Аристотель (384-322 рр. до н. е.) - давньогрецький учений-енциклопедист, основоположник формальної логіки. Основні твори в галузі логіки: «Категорії», «Про тлумачення», «Аналітики перша та
Базові висловлювання силогістики Висловлювання Позначення Інтерпретація Будь-який S є P "SÎ P Asp
Рішення силогізмів Силлогізм - висновок рангу 2, тобто. висновок, який можна зробити на підставі істинності двох посилок. У цих посилках фігурують три класи сутностей: S, P і M. Для формування силогізму використовують
Розширена силогістика Розширення класичної силогістики Аристотеля можливо зробити двома способами - переходом до негативних тверджень і збільшенням числа посилок.
Моделювання силлогістики Основний елемент при висновках у силлогістиці – перехід від двох посилок до висновку. Цей процес може бути автоматизований, схема автоматизованої системи для отримання силогістичних висновків
Синтаксис обчислення висловлювань Основне поняття обчислення висловлювань - висловлювання. Це пропозиції природною мовою, які можуть бути істинними чи хибними. При цьому розрізняють логічну істину мови
Поняття семантичного дерева Якщо Р = - безліч висловлювань, то семантичне дерево - це бінарне дерево, що задовольняє наступним умовам: 1) кожна дуга позначена негативною або поз
Алгоритм редукції Алгоритм редукції дозволяє довести загальнозначимість формул за допомогою приведення їх до протиріччя. Розглянемо роботу алгоритму з прикладу. Приклад. Перевірить
Нормальні форми таалгоритм нормалізації Кожна логічна формула може вивчатися алгебраїчно шляхом приведення її до нормальної форми. Можливе приведення до двох нормальних форм – кон'юнктивної нормальної форми (КНФ)
Алгоритм Куайну для ДНФ Алгоритм Куайну для ДНФ дозволяє перевірити здійсненність та загальнозначимість наведеної диз'юнктивної нормальної форми. Нехай р – елементарний вислів, а S – наведена
Принцип резолюцій У обчисленні висловлювань немає загального, по-справжньому ефективного критерію для перевірки здійсненності КНФ, проте є зручний метод виявлення нездійсненності безлічі диз'юнктів.
Алгоритм доказу нездійсненності логічної формули 1. Якщо у формулі немає нездійсненних диз'юнктів, то вибираються l, S1 і S2, такі, що l S1 і l S2. 2. Будується резольвента
Хорновські диз'юнкти Часто в обчисленні висловлювань виникає наступне завдання: потрібно перевірити якусь формулу (мету), логічно виведену з багатьох фактів і правил. Резолюція є методом доказу від
База знань на основі обчислення висловлювань Факти Формули обчислення висловлювань а1 – тварина має шерсть а2 – тварина годує дитинчат молоком а
Застосування обчислення висловлювань у конструюванні релейно-контактних схем Обчислення висловлювань знайшло широке застосування в теорії та практиці конструювання релейно-контактних схем завдяки основній властивості висловлювань – висловлювання може бути або істинним, або л
Обчислення предикатів Вже згадуваний вище силогізм «Люди смертні …» може бути представлений з допомогою обчислення висловлювань. Для його формалізації необхідно запровадити квантифіковану змінну
Визначення обчислення предикатів першого порядку Нехай заданодеяка множина M = , в якому m1, m2, …, mk – якісь певні предмети з цієї множини
Загальнозначимість і здійсненність формул обчислення предикатів Поняття загальнозначущості та суперечливості формул, введені в обчисленні висловлювань, зберігають свою силу і для обчислення предикатів. Формула обчислення предикатів називається
Обчислення предикатів як формальна система Розглянемо формальну аксіоматичну систему для обчислення предикатів. 1. Алфавіт: а) лічильна множина предметних змінних x1, x2, …, xn …;
Пренексні нормальні форми обчислення предикатів У обчисленні висловлювань було розглянуто дві нормальні форми висловлювань – КНФ і ДНФ. У обчисленні предикатів також є нормальна форма, так звана пренексна нормальна форма
Процедура виведення Ербрана У обчисленні предикатів немає універсального алгоритму, що дозволяє перевірити загальнозначимість, нейтральність, нездійсненність формули, т.к. для формули обчислення предикатів існує
Принцип резолюції для логіки предикатів У розділі 5 було викладено принцип резолюцій для обчислення висловлювань, де знаходження контрарних пар не викликало труднощів. Для логіки предикатів це негаразд. Справді, нехай є диз'юнкти т
Індуктивні міркування Термін «індукція» (від латів. inductio - наведення) в науку вперше був введений Аристотелем, який, у свою чергу, приписував перше застосування цього терміна Сократу. Арістот
Принцип єдиної відмінності «Якщо після введення деякого фактора з'являється або після видалення цього фактора зникає відоме явище, причому не вводилися і не видалялися ніякі інші фактори і не вироблялося ніякого
Особливості індуктивних схем міркувань Індуктивні міркування справедливі за умови, що в описі ситуації є безліч спостережуваних факторів і явищ. Причому в лівій частині причинно-наслідкового відношення може стояти
Алгоритм древ Даний алгоритм є методом якісного узагальнення за ознаками і запропонований як розвиток алгоритму узагальнення Е. Ханта - CLS. В основі методу використовується дерево рішень - один з
Індукція вирішальних дерев (ID3) Алгоритм ID3 (induction of decision tree) формує вирішальні дерева на основі прикладів. Кожен приклад має однаковий набір атрибутів (ознак), які можна розглядати
Метод фокусування Важливий крок під час вирішення завдання узагальнення понять – отримання вирішальних правил (продукцій, дерев), які містять як логічні функції на конкретних значеннях ознак, але включають більш
Міркування за аналогією Відповідно до Великого енциклопедичного словника «. аналогія (від грец. analogon – відповідність, рівність відносин) – подібність предметів (явлень, об'єктів) до будь-яких свій
Проста аналогія Дамо формальні механізми використання аналогії для вирішення завдань. Нехай існують два міркування: до першого входять два об'єкти S1 і S2, перетворення F і деякий висновок
Модальні логіки Вводяться оператори над логічними формулами, які можуть модифікувати їх інтерпретацію. Залежно від цього, які оператори вводяться, розрізняють класи модальних логік: 1.
Застосування нечіткої математики Вводиться поняття нечіткої множини – множини, щодо будь-якого з елементів якої можна зробити наступні висновки: 1. Елемент належить даному множині
Методи пошуку у просторі станів Методи пошуку у просторі станів фактичноє методами пошуку на графі, у якого початкова вершина – початковий стан, і заданий оператор, який будує всі вершини
Штучний нейрон Прагнучи відтворити функції людського мозку, дослідники створили прості апаратні (а пізніше програмні) моделі біологічного нейрона та системи його сполук. Коли нейрофізіологи
Персептрони Мал. 13. Персептронний нейрон Перше систематичне вивчення штучних нейронних мереж було зроблено Маккалокком
Навчання персептрону Здатність штучних нейронних мереж навчатися є їх найбільш інтригуючим властивістю. Подібно до біологічних систем, які вони моделюють, ці нейронні мережі самі моделюють себе в рез