Автоматично доказване на теорема

Нека има набор от формулиГ= A1,A2, …,An> и формулаВ.Автоматичното доказателство на теорема Bе алгоритъм, който проверява изходаA1,A2, …,An⊢B. Изразът гласи следното: "Ако предпоставкитеA1,A2, ...,Anса верни, тогава заключениетоB" е вярно.

Проблемът на доказателството в логиката е да се установи, че ако формулитеA1,A2, …,Anса верни, то формулатаBе вярна. Доказателството за това е равносилно на доказване на валидността на определена формула. Най-ефективното доказателство за валидността на формулите се извършва чрез метода на резолюциите. Процедурата за намиране на доказателство по метода на разделителната способност всъщност е процедура за намиране на опровержение, т.е. вместо да се доказва валидността на формулата, се доказва, че отрицанието на формулата е противоречиво.

При представяне на метода на резолюции обикновено се използва следната терминология.

Буквае изразътAили ØA. БуквитеAи ØAсе наричат ​​противоположни, а множеството A, ØA> –контра двойка.

Дизюнкте дизюнкция на букви (или елементарна дизюнкция). Една клауза се наричапразна(означена с ), ако не съдържа знаци. Празната клауза винаги е невярна, тъй като в нея няма знаци, които биха могли да бъдат верни за който и да е набор от променливи.

Нека разгледаме приложението на метода на резолюциите към пропозиционалното смятане.

Правило за разрешаванее името на следното правило за извод:

.

Правилото за разрешаване може да бъде записано като:AÚB, ØAÚC⊢BÚC.

Ако клаузите не съдържат контра знаци,тогава те нямат резолюция. За клаузиAи ØAрезолвентата е празна клауза:resA(A, ØA) = .

Алгоритъм за конструиране на изхода по метода на резолюциите.

Стъпка 1. Всички предпоставкиA1,A2, …,Anи формулата за отрицание на заключението ØBводят до CNF.

Стъпка 3. Извършете анализ на двойки на множествотоKкъм правилото: ако има дизюнктиDi,Dj, единият от коитоDiсъдържа променливатаAi, а другиятDjе отрицанието ØAi, тогава свържете тази двойка с логическа съединителна дизюнкцияDiÚD jи образуват, съгласно правилото за разделяне, нов дизюнкт - разделителна способност, като се изключват тези, съдържащи контразнациAiи ØAi.

Стъпка 4. Продължаваме процеса. Ако завършва с празна клауза, тогава заключението е оправдано.

Горният алгоритъм се наричаразрешително заключение от K.

Възможни са три случая.

1. Сред набора от клаузи няма съдържащи контракавички. Това означава, че формулатаBне може да бъде извлечена от набора от формулиA1,A2, …,An.

2. След следващото прилагане на правилото за разделяне се получава празна клауза. Това означава, че формулатаBможе да се извлече от набора от формулиA1,A2,…,An.

3. Процесът зацикля, т.е. получават се всички нови резолюции, сред които няма празни.

Кандидатствайте запример 3.2 A® (B®C),AÙB⊢Cметод за разрешаване. За да направите това, проверете изходаA® (B®C),AÙB, ØC⊢ .

ФормулиAÙB, ØCвече са в CNF.

Стъпка 2. Нека съставим набор отKклаузи:

Стъпка 3. Нека изградим разделително заключение отK. Нека напишем всичко по редклаузи отK:

Вместо чифт клаузи, съдържащи контралатерални знаци, ние пишем тяхната резолюция (номера на формулите, образуващи резолюцията, са дадени в скоби):

Заключението завършва с празна клауза, която оправдава заключениетоA® (B®C),AÙB⊢C.

Куестове

1. Установете правилността на разсъждението чрез конструиране на извеждането на пропозиционалното смятане.

2. Проверете изхода чрез метода на разделителна способност.

Варианти на индивидуални задачи

1. Тази организация се наема, ако преминете интервюто и ще бъдете сертифицирани положително. Не го приеха. Това означава, че или не е издържал интервюто, или не е бил положително атестиран.

Вариант #2

1. Ако светофарът е червен, значи преминаването е забранено. Пътуването е разрешено. Значи светофарът не свети червено.

Вариант #3

1. Ако триъгълникът е равностранен, то ъглите му са равни. Триъгълникът е равностранен. Следователно ъглите му са равни.

Опция #4

1. Ако обирът е извършен от Сидоров, значи той знае къде са откраднатите пари. Сидоров не знае къде са откраднатите пари. Следователно той не е извършил грабежа.

Вариант #5

1. Ако растението е лечебно, трябва да се пази. Това растение не е защитено. Следователно не е лекарствен.

Вариант #6

1. Петров инженер или студент. Той не е инженер. Следователно той е ученик.

Опция #7

1. Ако ученикът не учи систематично, значи няма солидни знания. Ако няма солидни познания, тогава няма да е добър специалист. Следователно, ако ученикът не учи систематично, тогава той няма да бъде добър специалист.

Опция #8

1. Това вещество може да бъдекиселина или сол. Това вещество не е сол. Следователно, това е киселина.

Опция #9

1. Ако линията докосва окръжността, тогава радиусът, начертан до точката на контакт, е перпендикулярен на нея. Радиусът на окръжността не е перпендикулярен на тази права. Следователно линията не докосва кръга.

Опция #10

1. Ако човек знае геометрия, значи знае Питагоровата теорема. Този човек не знае Питагоровата теорема. Следователно той не знае геометрия.

Опция #11

1. Ако една дума е поставена в началото на изречението, тогава тя се пише с главна буква. Тази дума се пише с малки букви. Следователно тази дума не се появява в началото на изречението.

Опция #12

1. Ако функцията е четна, тогава нейната графика е симетрична спрямо остаOY. Графиката не е симетрична спрямо остаOY. Следователно функцията не е четна.

Опция #13

1. Ако светофарът свети зелено, значи преминаването е разрешено. Пътуването не е разрешено. Значи светофарът не свети зелено.

Опция #14

1. Ако Андрей е отсъствал от работа, той не е изпълнил задачата. Андрей беше на работа. Следователно той изпълни задачата.

Опция #15

1. Лош е войникът, който не мечтае да стане генерал. Този войник е добър. Затова мечтае да стане генерал.

Опция #16

1. Ако триъгълникът е равностранен, значи е равнобедрен. Ако триъгълникът е равнобедрен, тогава ъглите в основата са равни. Следователно, ако триъгълникът е равностранен, тогава ъглите в основата са равни.

Опция #17

1. Ако диагнозата се потвърди, тогава той ще трябва да отиде в болницата. Ако отиде в болница, пътуването ще трябва да бъде отменено. Диагнозата се потвърди. Така че пътуването ще трябва да бъде отменено.

Опция #18

1. Петров е студент или ученик. Той не е ученик. Следователно той е ученик.

Опция #19

1. Ако съм уморен, не мога да се подготвя за час. Ако не мога да се подготвя за час, няма да напиша теста си. Уморен съм. Така че няма да пиша тестова работа.

Опция #20

1. Ако Сергей спечели състезанието, той ще влезе в националния отбор. Ако влезе в националния отбор, ще участва на Световното. Следователно, ако Сергей спечели състезанието, той ще участва в Световното първенство.

Тема 4. РАЗМИТА ЛОГИКА

Размитата логикасе различава от двузначната класическа логика по това, че акоистинните стойностина изявленията на класическата логика могат да бъдат само 0 („лъжа“) и 1 („вярно“), тогава размитата логика позволява безброй много междинни стойности на истината за изявления в интервала [0, 1].

Когато се описват сложни системи, в които наред с количествените данни има двусмислени качествени данни, трябва да се използват размити концепции и разсъждения. За да формализира такива проблеми, L. Zadeh разработи основите на математически апарат, базиран на концепциите заразмити множестваиразмита логика.

Основни концепции за размити множества

НекаM –е някакво множество, разгледайте някакво подмножествоAот това множество. За всякоxOMимамеxOAилиxWA.Можете да въведетехарактерна функцияна подмножествоA:

Тогава, например, акоM=a, b, c, d, e, f, g, h> иA=a, b, c, d>,имаме:

x	a	b	s	d	e	f	g	h
mA(x)

Набори, за които характеристичната функция приема само стойностите 0 или 1, ще се наричат ​​ясни.Класическата логика работи с ясни набори.

За размити множества характеристичната функция може да приеме произволна стойност от интервала [0,1]. Например,

x	a	b	s	d	e	f	g	h
mA(x)	1.0	0,1	0,8	0,7	0,5	0,2	0,0	0,1
mB(x)	0,1	0,3	0,8	0,9	0,5	0,1	0,0	0,0

За записване на размити множества се използва нотацията:A=х, mA (х))"xОM>. Нотацията характеризира степента на принадлежност на елементаxкъм множествотоA.

За размитите множества се дефинират отношенията на включване (Ì) и равенство (=):

Следните операции се извършват върху размити множества:

ДопълнениеA:

Пресичане:

Асоциация:

Елементи на размитата логика

Размито твърдениее твърдениеP,степен на истинностот коетоmPможе да бъде оценено с число от интервала [0, 1],mPn [0, 1].

Размитата пропозиционална променлива Xе размито твърдениеX, чиято степен на истинност може да варира в интервала [0, 1].

Тъй като степента на истинност на размито твърдение не е свързана със същността на твърдението, ние допълнително ще идентифицираме размито твърдение с неговата степен на истинностпо същия начин, по който едно обикновено ясно твърдение се отъждествява с неговата истинност или неистинност. Размитите твърдения и тяхната степен на истинност ще бъдат обозначени с букви:P,Q,Xи т.н.

Върху набора от размити предложения се въвеждат логически операции, които са подобни на операциите на пропозиционалната алгебра.

1.Отрицаниена размит оператор:ØP= 1 –P.

5.Еквивалентностна размити изрази:

Намерете степента на истинност на твърдението

Наборът от размити предложения заедно с въведените върху тях операции образуваталгебрата на размитите предложения.

Размитата логическа формуласе нарича:

1) всяка размита пропозиционална променлива;

2) акоPиQса размити логически формули, тогава ØP,PÙQ,PÚQ,P®Q,P»Qсъщо са размити логически формули;

3) няма други формули, освен тези, конструирани съгласно правилата на предходните два параграфа.

m(P,Q) = <P(a1, a2, …,an) «Q(a1, a2, …,an)>

Тук логическите операции на конюнкция и еквивалентност имат значението, дефинирано за логически операции върху размити изрази, а конюнкцията се приема за всички набори от степени на истинност (a1, a2, …, an) на размити променливи (X1,X2, …,Xn).

Акоm(P,Q) = 0,5, тогава размитите формулиPиQсе наричат ​​безразлични.

Акоm(P,Q)>gt; 0,5, тогава размитите формулиPиQсе наричат ​​размит еквивалент.

---