Автореферат (1137461), страница 3
Текст из файла (страница 3)
Í, ÈÄ, Â19. ÈÄ, ÊÃ→→23. ÀÒ, ÝÊÑ→→21. ÈÄ, Ì, ÎÁ22. Ì, ÀÒÈÄ, ÍÏ;→ÈÄ, ÍÏ, Ì;→ÊÃ;25. ÍÏ, ÀÒ→Ì;26. ÍÏ, ÎÁ→Í;ÈÄ;28. Í, Ì, ÎÁ→29. Ì, ÝÊÑ, ÊÏîëó÷åíàÎÀÎÁ;ÎÀÎÁ;24. Ì, ÝÊÑ→Ê, ÍÏ, ÊÃ;ÎÀÎÁ, Ñ;20. Ì, ÀÎÁ, ÎÁ27. Ì, ÊÎÀÎÁ, Ñ;ÎÀÎÁ, ÀÎÁ;→→Ñ;ÊÃ;→Á, ÈÍÒ.ñëåäóþùàÿäèàãðàììà12ðåøåòêèðàññìîòðåííûõÐèñ. 1: Äèàãðàììà ðåøåòêè êîíòåêñòà ôóíêöèé íà ìíîæåñòâàõM3èM2 ,M4ñâîéñòâ ôóíêöèé íà ìíîæåñòâàõ, ðèñ. 1.Âïðîöåññåèññëåäîâàíèÿîñíîâíîåâíèìàíèåáûëîóäåëåíîôóíêöèÿì íà ìíîæåñòâàõ ðàçìåðà 2 è 3.  ðàçäåëå 3.3.1 ïðåäñòàâëåíû ðåçóëüòàòû ïðîâåäåííîãî àâòîðîì èññëåäîâàíèÿ ðàçëè÷èé â èìïëèêàòèâíûõ òåîðèÿõ âçàèìîñâÿçåé ñâîéñòâ ôóíêöèé íà ìíîæåñòâàðàçìåðà 2 è 3.
Ñôîðìóëèðîâàíû è äîêàçàíû óòâåðæäåíèÿ, îáúÿñíÿþùåå âñå ðàçëè÷èÿ â èìïëèêàòèâíûõ òåîðèÿõ ýòèõ òèïîâ ôóíêöèé.Äëÿ ëþáîé ôóíêöèè f , îïðåäåë¼ííîé íà ìíîæåñòâå M2 , èç íàëè÷èÿ ñâîéñòâà Î ñëåäóåò íàëè÷èå ñâîéñòâà Ñ.Óòâåðæäåíèå 3.3.113Äëÿ ëþáîé ôóíêöèè f , îïðåäåë¼ííîé íà ìíîæåñòâå M2 , èç íàëè÷èÿ ñâîéñòâà ÈÍÒ ñëåäóåò íàëè÷èå ñâîéñòâàÑ.Óòâåðæäåíèå 3.3.2 ðàçäåëå 3.4 ïîêàçàíî, êàêèì îáðàçîì ìîæíî îáîáùèòü îïðåäåëåíèå ñâîéñòâ ôóíêöèé, à âìåñòå ñ òåì è ïîëó÷åííûå ðåçóëüòàòû,íà ñëó÷àé ôóíêöèé, çàäàííûõ íå íà ïðîèçâîëüíûõ ìíîæåñòâàõ, à íàðåøåòêàõ. ðåçóëüòàòå èññëåäîâàíèé, ïðåäñòàâëåííûõ â òðåòüåé ãëàâå,ïîëó÷åíû ñëåäóþùèå ðåçóëüòàòû.1.
Ðàçðàáîòàíû ìåòîäû àâòîìàòèçàöèè è ñòðóêòóðèçàöèè ïðîöåäóðû èññëåäîâàíèÿ èìïëèêàòèâíûõ âçàèìîñâÿçåé ñâîéñòâôóíêöèé íà ìíîæåñòâàõ. Èññëåäóåìûå âçàèìîñâÿçè ñòðóêòóðèðîâàíû â âèäå ðåøåòêè ïîíÿòèé, à òàêæå â âèäå áàçèñà èìïëèêàöèé. Ïðåäñòàâëåíû äîêàçàòåëüñòâà èìïëèêàöèé, ïîäãîòîâëåí ñïèñîê îòêðûòûõ èìïëèêàöèé.2. Ðàçðàáîòàí è ïðîãðàììíî ðåàëèçîâàí ìåòîä, ïîçâîëÿþùèé èçìåíÿòü âèä áàçèñà èìïëèêàöèé è îòîáðàçèòü èìïëèêàöèè â áîëåå óäîáíîé äëÿ ïðàêòè÷åñêèõ ïðèëîæåíèé ôîðìå.3. Ñôîðìóëèðîâàíû è äîêàçàíû ðàçëè÷èÿ ìåæäó èìïëèêàòèâíûìè òåîðèÿìè äëÿ ôóíêöèé íà äâóõ- è òðåõýëåìåíòíûõ ìíîæåñòâàõ.4.
Äàíî îáîáùåíèå ðåçóëüòàòîâ èññëåäîâàíèÿ ñâîéñòâ ôóíêöèéíà ñëó÷àé ôóíêöèé, çàäàííûõ íà ðåøåòêàõ.5. Ðàçðàáîòàíû è ïðîãðàììíî ðåàëèçîâàíû ìåòîäû, ïîçâîëÿþùèå àâòîìàòèçèðîâàòü ïðîöåññ ïîëó÷åíèÿ èìïëèêàòèâíûõ âçàèìîñâÿçåé ìåæäó ñâîéñòâàìè ôóíêöèé. Íàïèñàííîå ïðîãðàììíîå îáåñïå÷åíèå óäîâëåòâîðÿåò ñôîðìóëèðîâàííûì òðåáîâàíèÿì. êà÷åñòâå ïðåäìåòíîé îáëàñòè, ðåçóëüòàòû èññëåäîâàíèÿ êîòîðîé ïðåäñòàâëåíû â ÷åòâåðòîé ãëàâå, áûëè âûáðàíû àëãåáðàè÷åñêèå òîæäåñòâà, ïðåäñòàâëÿþùèå, âîçìîæíî, öåíòðàëüíûé èíòåðåñäëÿ óíèâåðñàëüíîé àëãåáðû.
 äàííîì èññëåäîâàíèè òðåáîâàëîñü14äîáèòüñÿ åùå áîëüøåé ñòåïåíè àâòîìàòèçàöèè, ÷åì ïðè èçó÷åíèèñâîéñòâ ôóíêöèè, òàê êàê êîëè÷åñòâî ïðåäñòàâëÿþùèõ èíòåðåñ äëÿïðèëîæåíèé òîæäåñòâ â ýòîì ñëó÷àå çíà÷èòåëüíî áîëüøå. Äëÿ ðàññìîòðåíèÿ áûëè âûáðàíû òîæäåñòâà, äëèíà êîòîðûõ íå ïðåâûøàåò 5(äëèíîé òîæäåñòâà íàçûâàåòñÿ ñóììà ÷èñëà âõîæäåíèé ïåðåìåííûõè îïåðàöèé). Òàêèõ òîæäåñòâ íàñ÷èòûâàåòñÿ 70.Îáëàñòü íàóêè, èçó÷àþùàÿ îáùèå çàêîíîìåðíîñòè àëãåáðàè÷åñêèõ ñèñòåì, íàçûâàåòñÿ óíèâåðñàëüíîé àëãåáðîé.íûìè êëàññàìèÝêâàöèîíàëü-â óíèâåðñàëüíîé àëãåáðå íàçûâàþò êëàññû àëãåáð,óäîâëåòâîðÿþùèõ çàäàííûì àëãåáðàè÷åñêèì òîæäåñòâàì. Ýêâàöèîíàëüíûå êëàññû èãðàþò â ýòîé îáëàñòè öåíòðàëüíóþ ðîëü.
 ðàçäåëå 4.1 ïðèâåäåíà êëþ÷åâàÿ òåîðåìà óíèâåðñàëüíîé àëãåáðû, ïîêàçûâàþùàÿ ýêâèâàëåíòíîñòü ìíîãîîáðàçèé àëãåáð è ýêâàöèîíàëüíûõêëàññîâ. ðàçäåëå 4.2 îïèñàíû ðàññìàòðèâàåìûå â ÷åòâåðòîé ãëàâå òîæäåñòâà. Àëãåáðàè÷åñêèå òîæäåñòâà, êàê è ñâîéñòâà ôóíêöèé íà ìíîæåñòâàõ, çàäàíû ñòðîãî ìàòåìàòè÷åñêè. Áîëåå òîãî, ïðîâåðêó óäîâëåòâîðåíèÿ êîíêðåòíîé àëãåáðîé êîíêðåòíîãî òîæäåñòâà ìîæíî àâòîìàòèçèðîâàòü. Ïîðîæäåíèå âñåõ àëãåáð íà íîñèòåëå îãðàíè÷åííîãî ðàçìåðà òàêæå ìîæíî àâòîìàòèçèðîâàòü. Ýòè çàäà÷è áûëè ðåøåíû àâòîðîì è ïðåäñòàâëåíû â ðàçäåëå 4.3.1.
Èçîìîðôèçì àëãåáðïîçâîëÿåò èçáåæàòü ïîðîæäåíèÿ òåõ àëãåáð, êîòîðûå çàâåäîìî íåìîãóò ïðèâíåñòè íîâîé èíôîðìàöèè.Èçó÷åíèå àëãåáðàè÷åñêèõ òîæäåñòâ ÿâëÿåòñÿ ïîäõîäÿùåé çàäà÷åé, ðåøåíèå êîòîðîé öåëåñîîáðàçíî ñ ïðèìåíåíèåì ìåòîäà èññëåäîâàíèå ïðèçíàêîâ, â òîì ÷èñëå ïîòîìó, ÷òî íà íàñòîÿùåå âðåìÿîòíîñèòåëüíî âûñîêîãî óðîâíÿ ðàçâèòèÿ äîñòèãëè èíñòðóìåíòàëüíûå ñðåäñòâà àâòîìàòè÷åñêîãî äîêàçàòåëüñòâà òåîðåì è íàõîæäåíèÿêîíå÷íûõ ìîäåëåé.
Äëÿ ýòèõ öåëåé â ïðîöåññå äèññåðòàöèîííîãî èññëåäîâàíèÿ èñïîëüçîâàëèñü ïðîãðàììûMace4 è Prover9, ðåøàþùèåïîñòàâëåííûå çàäà÷è áûñòðåå äðóãèõ ñðåäñòâ, êîòîðûå ìîãóò áûòüèñïîëüçîâàíû äëÿ òåõ æå öåëåé, è èìåþò óäîáíûé èíòåðôåéñ äëÿäîñòóïà ê íèì èç âíåøíèõ ïðîãðàìì.15Äîêàçàííûå â ðàçäåëå 4.3.2 óòâåðæäåíèÿ ïîêàçûâàþò, îäíàêî,÷òî ïîðîæäåíèÿ ëèøü àëãåáð íà êîíå÷íîì íîñèòåëå íåäîñòàòî÷íîäëÿ ïîñòðîåíèÿ èìïëèêàòèâíîé òåîðèè âûáðàííûõ àëãåáðàè÷åñêèõòîæäåñòâ. Çàäà÷à íàõîæäåíèÿ áåñêîíå÷íûõ àëãåáð, óäîâëåòâîðÿþùèõ çàäàííûì òîæäåñòâàì, êðàéíå òðóäîåìêà è â îáùåì ñëó÷àå íåèìååò ðåøåíèÿ.
Àâòîðó óäàëîñü íàéòè ìåòîäû ïîðîæäåíèÿ àëãåáðíà áåñêîíå÷íîì íîñèòåëå, íåîáõîäèìûå äëÿ çàâåðøåíèÿ èññëåäîâàíèÿ, à òàêæå - ïðîãðàììíî ðåàëèçîâàòü ýòè ìåòîäû (ðàçäåë 4.3.3).Çàäà÷à ïîðîæäåíèÿ àëãåáð íà áåñêîíå÷íîì íîñèòåëå ñòàâèòñÿA → b, A ⊆ Mid , b ∈A = (N, ∗, −, a), êîòî-ñëåäóþùèì îáðàçîì.
Ïóñòü äàíà èìïëèêàöèÿMid .Òîãäà íåîáõîäèìî íàéòè òàêóþ àëãåáðóðàÿ óäîâëåòâîðÿåò âñåì òîæäåñòâàì èçäåñòâóAè íå óäîâëåòâîðÿåò òîæ-b.Äëÿ íàõîæäåíèÿ òàêèõ àëãåáð áûëà çàôèêñèðîâàíà ôîðìà áèíàðíîé, óíàðíîé è íóëÿðíîé îïåðàöèé. Íóëÿðíàÿ îïåðàöèÿ âñåãäàôèêñèðîâàëàñü ðàâíîé íóëþa = 0. Óíàðíàÿ îïåðàöèÿ − èñêàëàñü âñëåäóþùåì âèäå:u0 ,u ,1−n =u2 ,p × n + q,ãäååñëèåñëèåñëèåñëèn = 0;n = 1;n = 2;n ≥ 3,u0 , u1 , u2 ∈ N<5 , p ∈ N<3 , q ∈ {0, 1, −1, 2, −2, 3, −3}.16Áèíàðíàÿ îïåðàöèÿ∗èñêàëàñü â ñëåäóþùåì âèäå:b00 ,b01 ,b10 ,b11 ,b02 ,b03 ,b12 ,b13 ,b20 ,b30 ,b21 ,m ∗ n = b31 ,b22 ,c0 × m + d0 × n + e0 ,c1 × m + d1 × n + e1 ,c2 × m + d2 × n + e2 ,c3 × m + d3 × n + e3 ,c4 × m + d4 × n + e4 ,c5 × m + d5 × n + e5 ,c6 × m + d6 × n + e6 ,c7 × m + d7 × n + e7 ,c8 × m + d8 × n + e8 ,c9 × m + d9 × n + e9 ,ãäååñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèåñëèm=0m=0m=1m=1m=0m=0m=1m=1m=2m=3m=2m=3m=2m=0m=1m>3m>3m>2m>1m>2m>1m>3m>4èèèèèèèèèèèèèèèèèèèèèèèn = 0;n = 1;n = 0;n = 1;n = 2;n = 3;n = 2;n = 3;n = 0;n = 0;n = 1;n = 1;n = 2;n > 3;n > 3;n = 0;n = 0;m = n;n = m + 1;n = m − 1;n = m + 2;n = m − 2;n 6= m, m ± 1, m ± 2,b00 , b01 , b10 , b11 ∈ N<4 ,b02 , b03 , b12 , b13 , b12 , b13 , b20 , b30 , b22 ∈ N<6 ,c0−9 , d0−9 ∈ {0, 1}, e0−9 ∈ {0, 1, −1, 2, −2, 3, −3}.17Âñå èìïëèêàöèè, ê êîòîðûì íå áûëè íàéäåíû êîíòðïðèìåðû âçàäàííîì âèäå, áûëè äîêàçàíû.
Òàêèì îáðàçîì, òàêîé âûáîð ñòðóêòóðû àëãåáð ïîçâîëèë íàéòè âñå íåîáõîäèìûå êîíòðïðèìåðû.Äëÿ íàõîæäåíèÿ àëãåáð â çàäàííîì âèäå àâòîðîì äèññåðòàöèèïðåäëîæåí àëãîðèòì ïîèñêà ñ âîçâðàòîì.⊆ Mid , id_conc ∈ Mid .Àëãåáðà A ñèãíàòóðû (∗, −, 0),Input: idls_premOutput:óäîâëåòâîðÿþùàÿòîæäåñòâàì idls_prem è íå óäîâëåòâîðÿþùàÿòîæäåñòâó id_conc.1234567891011121314True dofor id in idls_premwhiledosat, eld = check_identity_partial(A, id)ifsat = Falsethenbacktrack(A)breakifsat = None thenupdate(A, eld)breakelsesat, eld = check_identity_partial(A, id_conc)ifsat = Truethenbacktrack(A)continue151617if1819ifsat = None thenupdate(A, eld)continuesat = Falsereturn AthenÀëãîðèòì 1: nd_algebraÏîñòðîåíèå èìïëèêàòèâíîé òåîðèè àëãåáðàè÷åñêèõ òîæäåñòâóäàëîñü ïîëíîñòüþ çàâåðøèòü, äîêàçàâ âñå èìïëèêàöèè, íàõîäÿùè-18åñÿ â êàíîíè÷åñêîì áàçèñå èìïëèêàöèé ïîñòðîåííîãî êîíòåêñòà. Ðåçóëüòàòû èññëåäîâàíèÿ ïðåäñòàâëåíû â ðàçäåëå 4.4.
Ïðîãðàììíûéêîä, òåñòû ê ïðîãðàììíîìó êîäó, ïîëó÷èâøèéñÿ êîíòåêñò, áàçèñ èìïëèêàöèé, à òàêæå äîêàçàòåëüñòâà èìïëèêàöèé èç áàçèñà èìïëèêàöèé âûíåñåíû â ïðèëîæåíèå ê äèññåðòàöèîííîé ðàáîòå. Òðåáîâàíèÿ,ïðåäúÿâëÿåìûå ê ðàçðàáîòàííûì è ðåàëèçîâàííûì àâòîðîì ìåòîäàì, çàêëþ÷àëèñü â ñëåäóþùåì: ïîñòðîèòü èìïëèêàòèâíóþ òåîðèþ70 âûáðàííûõ òîæäåñòâ è ïîëó÷èòü äîêàçàòåëüñòâà âñåõ èìïëèêàöèé èç áàçèñà èìïëèêàöèé.
Òðåáîâàíèÿ áûëè âûïîëíåíû. ïðîöåññå âûïîëíåíèÿ èññëåäîâàíèÿ èìïëèêàòèâíîé òåîðèèàëãåáðàè÷åñêèõ òîæäåñòâ äîñòèãíóòû ñëåäóþùèå îñíîâíûå ðåçóëüòàòû.1. Ïîëó÷åíî ðàçâèòèå ïîäõîäîâ, ðàíåå èñïîëüçóåìûõ äëÿ àâòîìàòèçàöèè ïðîöåññîâ ïîñòðîåíèÿ èìïëèêàòèâíîé òåîðèè ñâîéñòâôóíêöèé íà ìíîæåñòâàõ. Ðàçðàáîòàíû ìåòîäû àâòîìàòèçàöèèïîñòðîåíèÿ èìïëèêàòèâíîé òåîðèè àëãåáðàè÷åñêèõ òîæäåñòâ.2. Ðàçðàáîòàíû è ïðîãðàììíî ðåàëèçîâàíû àëãîðèòìû, êîòîðûåïîçâîëÿþò ïðîâåðèòü, óäîâëåòâîðÿþòñÿ ëè òîæäåñòâà, à òàêæå ïîðîæäàòü íåèçîìîðôíûå àëãåáðû íà êîíå÷íûõ íîñèòåëÿõ.3.
Ðàçðàáîòàí ìåòîä è ðåàëèçîâàí àëãîðèòì íàõîæäåíèÿ àëãåáðûíà áåñêîíå÷íîì íîñèòåëå, óäîâëåòâîðÿþùåé íåêîòîðîìó ìíîæåñòâó òîæäåñòâ è íå óäîâëåòâîðÿþùåé îäíîìó âûáðàííîìóòîæäåñòâó.4. Ñ èñïîëüçîâàíèåì òîëüêî ïðîãðàììíûõ ñðåäñòâ ïîñòðîåíà èìïëèêàòèâíàÿ òåîðèÿ äëÿ âñåõ 70 àëãåáðàè÷åñêèõ òîæäåñòâ äëèíû íå áîëåå 5. Ñîçäàííîå ïðîãðàììíîå îáåñïå÷åíèå óäîâëåòâîðÿåò ïðåäúÿâëÿåìûì ê íåìó òðåáîâàíèÿì. ãëàâàõ 3 è 4 ïîÿâëåíèå îøèáîê â ñîäåðæàíèÿõ îáúåêòîâ óäàëîñü èñêëþ÷èòü âñëåäñòâèå òîãî, ÷òî ìàòåìàòè÷åñêè îïðåäåëåíûïðèçíàêè êîíòåêñòîâ è àëãîðèòìèçèðîâàíà èõ ïðîâåðêà. Îäíàêî ïîêàçàíî, ÷òî íå âî âñåõ ñëó÷àÿõ òàêîå âîçìîæíî.
Íàïðèìåð, èíôîðìàöèÿ î ñâÿçÿõ îáúåêòîâ è ïðèçíàêîâ, íàéäåííàÿ â ãëîáàëüíîé ñåòèÈíòåðíåò, íå ìîæåò ñ÷èòàòüñÿ íàäåæíîé è îòñóòñòâèå îøèáîê ãà-19ðàíòèðîâàòü íåëüçÿ.  ñëó÷àå ïðîâåäåíèÿ èññëåäîâàíèé ìåòîäàìèÀÔÏ â ïîëèòîëîãèè, ýêñïåðòû íå âñåãäà ìîãëè ñîéòèñü âî ìíåíèèîòíîñèòåëüíî òîãî èëè èíîãî îáúåêòà è ïðèçíàêà.Åùå áîëåå îñòðî íåîáõîäèìîñòü ðåøåíèÿ çàäà÷è íàõîæäåíèÿîøèáîê â íîâûõ îáúåêòàõ êîíòåêñòà âñòàåò òîãäà, êîãäà ïðåäïîëàãàåòñÿ îäíîâðåìåííûé äîñòóï ê êîíòåêñòó íåñêîëüêèìè ïîëüçîâàòåëÿìè.  òàêîì ñëó÷àå íåêîòîðûå ïîëüçîâàòåëè ìîãóò ïîïûòàòüñÿíàìåðåííî èñïîðòèòü èññëåäîâàíèå ïóòåì äîáàâëåíèÿ íîâûõ îáúåêòîâ, ñîäåðæàùèõ îøèáêè.
Íà íàñòîÿùåå âðåìÿ â ðàìêàõ ÀÔÏ íåïðåäëîæåíî íè îäíîãî ïîäõîäà ê ðåøåíèþ ýòîé çàäà÷è. Ìåòîä íàõîæäåíèÿ îøèáîê â íîâûõ îáúåêòàõ êîíòåêñòà ìîã áû ðàñøèðèòüîáëàñòü ïðèìåíåíèÿ ÀÔÏ íà áîëåå øèðîêèé êðóã çàäà÷, â òîì ÷èñëå íà îïèñàííûå âûøå, è, òåì ñàìûì, ñïîñîáñòâîâàòü ïîÿâëåíèþíîâûõ âîçìîæíîñòåé äëÿ èõ ðåøåíèÿ. ðàìêàõ ÀÔÏ íåò íèêàêèõ âíóòðåííèõ îãðàíè÷åíèé íà ñîäåðæàíèÿ îáúåêòîâ, ïîýòîìó ëþáîé îáúåêò ìîæåò èìåòü ëþáîå ñîäåðæàíèå, íà÷èíàÿ îò ïóñòîãî ìíîæåñòâà è çàêàí÷èâàÿ âñåì ìíîæåñòâîì ïðèçíàêîâ. Òàêèå îãðàíè÷åíèÿ ìîãóò, îäíàêî, áûòü ïðèñóùèïðåäìåòíîé îáëàñòè, à, ñëåäîâàòåëüíî, ÿâëÿþòñÿ âíåøíèìè ïî îòíîøåíèþ ê ÀÔÏ. Êîíå÷íî, íè÷òî íå ìåøàåò èñïîëüçîâàòü âíåøíèåîãðàíè÷åíèÿ ïðè äîáàâëåíèè íîâûõ îáúåêòîâ ê êîíòåêñòó.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
