Стандартните форми на Сколем за смятане на предикати
Стандартни форми на смятане на предикати на Сколемов - раздел Обучение, Основни понятия и определения
Очевидно е, че ако формулите F и Ф са еквивалентни, тогава F е логически неудовлетворима тогава и само ако Ф е логически неудовлетворима. Благодарение на това твърдение и поради факта, че редукционните алгоритми в PNF запазват еквивалентността на неудовлетворимите формули, в по-нататъшни процедури за доказване можем да се ограничим до формули, които имат предварителна форма и дори още по-тесен клас формули, така наречената "-форма улас.
Формула F се нарича "-формула, ако е представена в PNF, а кванторната част се състои само от универсални квантори, т.е.
F \u003d "x1"x2 ... "xr M, където M е формула без квантор.
По този начин възниква проблемът с елиминирането на екзистенциалните квантори във формулите, представени в PNF. Това може да стане чрез въвеждане наSkolem функции.
Нека формулата е представена в PNF и нека zi (1£ i £ r) е кванторът на съществуване в префикса. Ако i = 1, т.е. нито един универсален квантор не предхожда квантора на съществуване, тогава се избира константаcот областта на M, различна от константите, срещащи се в M, и x1 се заменя сcв M. Кванторът на съществуване z1x1 се изтрива от префикса. Ако кванторът на съществуване zi е предшестван отmуниверсални квантори, тогава се избира m-имен функционален символ f, различен от функционалните символи в M, и xi се заменя от функцията f(xj1, xj2, … xjm), наречена функция на Skolem. Екзистенциалният квантор zi xi отпада от префикса.
Алгоритъмът за последователно изключване на екзистенциални квантори от PNF, базиран на описаната процедура, се наричаалгоритъмSkolem :
1. Изпратете формулата в PNF.
2. Намерете най-малкия индекс i, така че z1z2 ... zi-1 всички да са равни ", но zi = $. Ако i = 1, тогава вместо x1 във формулата M заместете константатаc, различна от константите, срещащи се в M. Ако няма такова i, тогава формулата F е "-формула.
3. Вземете нов (i -1)-локален функционален символ fi, който не се намира във F, и заменете xi с fi (x1, ..., xi-1). Отидете на стъпка 2.
Преходът от формула в PNF към "-формула не засяга свойството на формулата да бъде неудовлетворима. По този начин алгоритъмът на Skolem, запазвайки свойството на неудовлетворимост, редуцира произволна формула, която има предварителна форма, до "-формула.
Частта от формулата без квантификатор (матрица) трябва да се редуцира до CNF. Алгоритъмът за еквивалентно преобразуване на произволна формула без квантори в CNF е подобен на алгоритъма, описан в пропозиционалното смятане.
И така, чрез последователно прилагане на редукция до PNF, Skolem и редукция до CNF алгоритми със запазване на свойството невъзможност, всяка формула F може да бъде представена чрез набор от клаузи, обединени от универсални квантори. Такава формула се нарича формула,представена в стандартен формуляр на Сколемов (SSF).
Пример. Приведете формула F към SSF.
1. F = "x [P(x) Ù "y $x (¬¬Q(x,y) Ú "z R(a,x,y))].
2. "x "y $u [P(x) u (Q(u,y) Ú R(a,u,y))].
4. "x "y [P(x) Ù (Q(f(x,y),y) Ú R(a, f(x,y),y))].
Тази тема принадлежи към раздела:
Основни понятия и определения
В момента изкуственият интелект е една от бързо развиващите се области на науката, която разработва методи и инструменти за намиране на решения Идеята за създаване на изкуствено подобие на човешкия ум за решаване на сложни проблеми.Един приятел разви тази идея, като предложи..
Какво ще правим с получения материал:
Всички теми в този раздел:
Концепцията за изкуствен интелект Централната концепция е концепцията за „изкуствен интелект“. Терминът изкуствен интелект е предложен през 1956 г. на научен семинар в Станфорд
Попов Е.В., Фирдман Г.Р. (Алгоритмични основи на интелигентни роботи и изкуствен интелект, 1992) „ИИ система се разбира като система, която има способността да натрупва и коригира знания въз основа на активното възприемане на информация за света и целенасочено поведение въз основа на натрупаните
Цели и задачи на изкуствения интелект Основните цели на изкуствения интелект включват: 1. Обработка на визуални сцени: - обработка на изображения; - разпознаване и разбиране на модели; - машина
Произход на формалното разсъждение 2.1. Мислене на ляво и дясно полукълбо Както знаете, човешкият мозък се състои от две полукълба, всяко от които преобразува информацията по свой начин. Целият свят е разделен
Видове мислене Лявото полукълбо - "Аз" Тип мислене Сходство - разлика Идентифициране на характеристики на конкретни обекти Разлагане на цялото на части
Разрешимост на формална система Първият въпрос, който възниква при определянето на формална система, е въпросът за инверсията, т.е. дали е възможно, като се има предвид всяка формула на формална система, да се определи дали
Тълкуване на формална система Формалните системи не са просто игра на ума, но винаги са модел на някакъв вид реалност (конкретна или математическа). Тълкуване на репрезентации
Доказателство и истина От горните определения вече има aизграждане на дълбоко разграничение между понятията доказателства и истина. Тези концепции принадлежат към две различни области. Априори нищо не е гара
Основни принципи на силогистиката Аристотел (384-322 г. пр. н. е.) - старогръцки енциклопедист, основоположник на формалната логика. Основните произведения в областта на логиката: "Категории", "За интерпретацията", "Аналитиците първо и
Основни твърдения на силогистиката Изявление Обозначение Тълкуване Всяко S е P "SÎ P Asp
Решение на силогизмите Силогизмът е заключение от ранг 2, т.е. заключението, което може да се направи от истинността на две предпоставки. Три класа същности се появяват в тези предпоставки: S, P и M. За да се образува силогизъм,
Разширена силогистика Класическата силогистика на Аристотел може да бъде разширена по два начина - чрез преминаване към отрицателни твърдения и чрез увеличаване на броя на помещенията.
Моделиране на силогистиката Основният елемент в заключенията в силогистиката е преходът от две предпоставки към заключение. Този процес може да бъде автоматизиран, схема на автоматизирана система за получаване на силогистични заключения
Синтаксис на пропозиционалното смятане Основната концепция на пропозиционалното смятане е пропозиция. Това са изречения на естествен език, които могат да бъдат верни или неверни. В същото време се отличава логическата истинност на езика
Концепцията за семантично дърво Ако Р= е набор от твърдения, тогава семантичното дърво е двоично дърво, което отговаря на следните условия: 1) всяка дъга е отбелязана с отрицателна или поз.
Алгоритъм за редукция Алгоритъмът за редукция ни позволява да докажем валидността на формулите, като ги сведем до противоречие. Разгледайте работата на алгоритъма на пример. Пример.Проверете
нормални форми иалгоритъм за нормализиране Всяка логическа формула може да се изучава алгебрично чрез редуцирането й до нормална форма. Възможно е да се редуцира до две нормални форми - конюнктивна нормална форма (CNF)
Алгоритъмът на Куайн за DNF Алгоритъмът на Куайн за DNF ви позволява да проверите изпълнимостта и валидността на намалената дизюнктивна нормална форма. Нека p е елементарно предложение, а S редуцирано
Принципът на разрешаване В пропозиционалното смятане няма общ, наистина ефективен критерий за тестване на удовлетворимостта на CNF, но има удобен метод за откриване на неудовлетворимостта на набор от клаузи.
Алгоритъм за доказване неприложимостта на логическата формула 1. Ако във формулата няма неудовлетворими клаузи, тогава l, S1 и S2 се избират така, че lÎ S1 и ù lÎ S2. 2. Резолвентата е конструирана
Хорн клаузи Често в пропозиционалното смятане възниква следният проблем: трябва да проверите някаква формула (цел), логически извлечена от набор от факти и правила. Резолюцията е метод за доказване от
База знания за пропозиционално смятане Факти Формули за пропозиционално смятане a1 - животното има коса a2 - животното храни малките си с мляко a
Използването на пропозиционално смятане при проектирането на релейно-контактни вериги Пропозиционалното смятане намери широко приложение в теорията и практиката на проектиране на релейно-контактни вериги поради основното свойство на предложенията - едно предложение може да бъде или вярно, или l
Смятане на предикатите Силогизмът „Хората са смъртни…“, вече споменат по-горе, не може да бъде представен чрез смятане на изказванията. За неговото формализиране е необходимо да се въведе количествено определена променлива
Дефиниция на предикатно смятане от първи ред Нека е даденонякакво множество M = , в което m1, m2, …, mk са някои специфични обекти от това множество
Обща валидност и изпълнимост на формулите на предикатното смятане Концепциите за валидност и непоследователност на формулите, въведени в пропозиционалното смятане, остават валидни и за предикатното смятане. Формулата за изчисляване на предикатите се нарича
Предикатното смятане като формална система Нека разгледаме формална аксиоматична система за предикатното смятане. 1. Азбука: а) изброим набор от предметни променливи x1, x2, …, xn …;
Пренексни нормални форми на изчислението на предикатите В пропозиционалното смятане бяха разгледани две нормални форми на изявленията - CNF и DNF. Считането на предикатите също има нормална форма, така наречената пренексна нормална форма
Процедура за извеждане на Herbrand В изчислението на предикатите няма универсален алгоритъм, който ви позволява да проверите валидността, неутралността и невъзможността на формула, т.к. за формулата на предикатното смятане има
Принципът на разделителна способност за предикатната логика В Глава 5 беше въведен принципът на разделителна способност за пропозиционално смятане, където намирането на контра-двойки не беше трудно. Това не е така за логиката на предикатите. Наистина, нека има клаузи m
Индуктивно разсъждение Терминът "индукция" (от латински inductio - насочване) е въведен за първи път в науката от Аристотел, който от своя страна приписва първото използване на този термин на Сократ. Аристот
Принцип на единичната разлика „Ако след въвеждането на фактор известно явление се появи или изчезне след премахването на този фактор и не се въвеждат или премахват други фактори и не
Характеристики на схемите за индуктивно разсъждение Индуктивното разсъждение е валидно при условие, че в описанието на ситуацията има пълен набор от наблюдаеми фактори и явления. Освен това от лявата страна на причинно-следствената връзка може да има
Дървовиден алгоритъм Този алгоритъм е метод за качествено обобщение по признаци и се предлага като развитие на алгоритъма за обобщение на Е. Хънт - CLS. Методът се основава на дърво на решенията, едно от
Индукция на дървета на решения (ID3) Алгоритъмът ID3 (индукция на дърво на решения) генерира дървета на решения въз основа на примери. Всеки пример има един и същ набор от атрибути (характеристики), които могат да бъдат разгледани
Метод на фокусиране Важна стъпка в решаването на проблема с обобщаването на концепцията е получаването на правила за вземане на решения (продукции, дървета), които съдържат не само логически функции върху специфични стойности на признаци, но включват повече
Разсъждение по аналогия Според Големия енциклопедичен речник “. аналогия (от гръцки analogon - съответствие, равенство на отношенията) - сходството на обекти (явления, обекти) във всеки
Проста аналогия Нека дадем формални механизми за използване на аналогия за решаване на проблеми. Нека има два аргумента: първият включва два обекта S1 и S2, трансформация F и някакво извеждане
Модални логики Въведени са оператори на логически формули, които могат да променят тяхната интерпретация. В зависимост от въведените оператори има класове модални логики: 1.
Приложение на размитата математика Въвежда се понятието размито множество - множество, по отношение на всеки от елементите на което могат да се направят следните заключения: 1. Даден елемент принадлежи на дадено множество
Методи за търсене в пространство на състояния Всъщност методи за търсене в пространство на състоянияса методи за търсене на граф, чийто начален връх е началното състояние и е даден оператор, който изгражда всички върхове, които не следват
Изкуствен неврон В опит да възпроизведат функциите на човешкия мозък, изследователите създадоха прости хардуерни (и по-късно софтуерни) модели на биологичен неврон и неговите системи за взаимно свързване. Кога постигнаха неврофизиолозите
Перцептрони Фиг. 13. Персептрон неврон Първото систематично изследване на изкуствени невронни мрежи е предприето от McCulloch
Обучение на перцептрон Способността на изкуствените невронни мрежи да учат е най-интригуващото им свойство. Подобно на биологичните системи, които моделират, тези невронни мрежи се моделират в реално време.