15. Пнф. Алгоритъм за намаляване на pnf.
За да се улесни анализът на сложни твърдения, формулите на предикатната алгебра се препоръчват да бъдат редуцирани до нормална форма. Ако в алгебрата на предложенията се приемат две нормални форми (DNF - дизюнктивна и CNF - конюнктивна), то в алгебрата на предикатите - еднапренексна нормална форма(PNF), чиято същност е да раздели формулата на две части: квантор и неквантор. За да направите това, всички квантори на формулата се изваждат отляво, като се използват законите и правилата на предикатната алгебра.
В резултат на тези алгебрични трансформации може да се получи формула от вида: x1 x2 xn(M), където , а M е матрицата на формулата. Кванторната част на формулата x1 x2 xn понякога се нарича PNF префикс.
Стъпка 1. Елиминирайте логическите връзки и навсякъде
Стъпка 2. Насърчаване на отрицанието до елементарна формула
Стъпка 3. Преименувайте обвързаните променливи според правилото:
„намерете най-лявата поява на обектна променлива, така че тази поява да е обвързана с някакъв квантор, но има друго поява на същата променлива; след това направете замяната на асоциираното събитие с появата на новата променлива “, повторете операцията, докато замяната на асоциираните променливи стане възможна;
Стъпка 4. Преместете кванторите наляво според законите на алгебрата на логиката.
Стъпка 5. Преобразувайте матрицата без квантори в CNF.
16. Ssf. Алгоритъм за измама.
За да се елиминират кванторите на съществуване от префикса на формулата, беше разработен алгоритъмът Skolem, въвеждащфункцията Skolemза свързване на обектната променлива на квантора на съществуване с други обектни променливи.
Стъпка 1. Представете формулатаFкато PNF.
Стъпка 2. Намерете най-левия екзистенциален квантор в префикса:
а) ако кванторът е на първо място от префикса, тогава вместо променливата, обвързана от екзистенциалния квантор,заменете навсякъде предметната константаa, която е различна от срещащите се предметни константи в матрицата на формулата, и премахнете екзистенциалния квантор;
б) ако квантификаторът не е на първо място на префикса, т.е.x1x2xi-1xi . след това изберете (i-1)-имен функционален символ, различен от функционалните символи на матрицата M и заменете обектната променлива xi, обвързана от квантора на съществуване, с функцията f(x1;x2 ; xi-1) и изтрийте квантора на съществуване.
Стъпка 3. Намерете следващия екзистенциален квантор вдясно и отидете на стъпка 2, в противен случай край.
PNF формулата, получена в резултат на въвеждане на функцията на Skolem, се наричастандартна форма на Skolem на формулата (SSF).
17. Смятане на предикатите. Уводни бележки, тълкуване на формули.
Всички методи и резултати от пропозиционалното смятане могат да бъдат прехвърлени към предикатното смятане, т.е. всяка теорема и всяко извеждане на пропозиционалното смятане става теорема и производно на предикатното смятане, ако пропозиционалните променливи се заменят с формули на предикатния език и всички появявания на една и съща променлива се заменят навсякъде с една и съща формула. Всяка схема на теоремата и всяка схема на извод също се запазват, ако под знаците на пропозиционалните променливи се вземат формули на езика на предикатите.
За да се формализира процесът на разсъждение в изчислението на предикатите, е необходимо да се отдели клас формули, които определят техните еквивалентни трансформации в присъствието на квантори, и клас отношения между формули, които образуват последователна верига от формули от предпоставки до заключение. Трябва да се отбележи, че правилата, аксиомите и законите на пропозиционалното смятане са подмножество от правилата, аксиомите и законите на предикатното смятане. Допълнителни правила, аксиоми изаконите определят възможностите за въвеждане и премахване на квантори, замяна и промяна на квантори.
Подинтерпретациятрябва да се разбира система, състояща се от непразно множество V, нареченовселена,и еднозначно преобразуване върху набор от два елемента, което присвоява на всеки предикатен символ P n (t1; t2; tn) n-локална релация в множеството V, към всеки функционален символ f n i (t1; t2; tn ) - n-местна операция върху множеството V, всяка обектна константа е елемент от множеството V.
Формула, която не съдържа свободни променливи, се наричазатворенаи представлява изявление за елементи, функции и релации, което приема стойността и или l.
Формула, съдържаща свободни променливи, се наричаopenи представлява релация, дефинирана в множеството V,
Тази връзка може да е вярна за някои стойности в областта на интерпретацията и невярна за други.
Идентично верни формули(или тавтологии) са специален клас формули за изчисляване на предикати, които приемат стойността на „истина“ за всички интерпретации на константите на предмета, функционалните и предикатните символи, включени в него; тези формули играят ролята на законите и аксиомите на предикатното смятане; всякакви замествания и замествания в идентично вярна формула не променят нейния смисъл.
Идентично неверни формули(или противоречие) е специален клас от формули за изчисляване на предикати, които приемат стойността „лъжа“ за всички интерпретации на константите на предмета, функционалните и предикатните символи, включени в него; всякакви замествания и замествания в идентично невярна формула не променят нейния смисъл.
Изпълними формулие специален класформули за предикатно смятане, които приемат стойността „истина“ в някакъв домейн, т.е. не за всички интерпретации на константите на предмета, функционалните и предикатните символи, включени в него.