- Формальды логикада дұрыс ой тұжырымдамалары зерттеліп,локикалық дәйекті формада дайындалады.Математикалық модульдерді логикаға қолдануға,мысалы,түрлі символдарды, шығару ержелерін пайдаланып,формальды жүйенің есептері ретінде қарастыруға болады.
Жалпы, формальды жүйе деп сыртқы дүниеге қатысы жоқ,формальданылған нысандар(объектілер) жиынтығын атайды.Ол мағынасы алдын ала анықталған ережелер(өнімдік әдістер,фреймдер,т.б.) не символдар жиынынантұрыуы мүмкін.
Мынадай пукттер белгілі кезде формальды жүйе анықталған деп есептеледі
1.Шектеулі алфавит берілген (алфавит тұрақтылар,айнымалылар және операторлардан тұрыуы мүмкін)
- Жүйенің ұйғарым, өрнек (формулалар)құратын процедурасы анықталған.
- Бір шама формулалар жиынтығы (фактілер) алдын ала ақиқат түрде белгіленген (олар аксиома деп аталады).
4.Шығару ережелерінің шектелу жиыны берілген.Олар арқылы бір формулалар жиынынан екінші формулалар жиынына көшіуге болады.Шығару ережелері мынадай түрде берілуі мүмкін
U1 ,U2 ,…,Up W1,W2,…,Wn
Мұндағы Uk,Wk (k=1.2,..) формальды жүйенің формулалары,нұсқама()-импликация (ілестіру) белгісі (импликация жөнінде 3,2- тақырыпты қараңыз).
Ескерту.ЖИ-де пайдаланылатын кейбір терминдер:
-Тұжырым жасауда “егер, онда, немесе, және, олай болса ” сияқты пайдаланылатын тұрақты сөздерді типтік сөздер,операторлар деп атайды.
-Формула –дұрыс құрылған символдар тізбегі (ол-әдеттегідей өрнек не ұйғарым).Егер формуланы дәлелдеу мүмкін болса, ол теорема делінеді.
—Процедура-шектеулі қадамдар бойынша нәтиже алуға болатын фактілер мен ережелер топтамасы.
—Шығару ережесі-бір пікірден екінші пікір алу ережесі.
—Білімді көрсету –келелі мәселенің шешімін ыңғайлы түрде іздеу үшін білімді құрлымды түроде сипаттау.
- -Формальды жүйе тәсілін пайдаланып, тригонометриалық теңдеулерді шешу үшін 1947-жылы М.Grandbastien дайындалған PRET атаулы процедураны қарастырайық.Онда теңдеу P(trigo(x))=const түрінде алынған.Мұндағы P(trigo(x)) аргументі х болатын тригонометриялық sin, cos, tg, ctg фукцияларынан тұратын полином.Мұндай есептерді шешу үшін мынадай екі типті теңдеулерді қалай шешеу жолы программаға білім қоры ретінде енгізіліп қойылған:
trigo(x)=c,(B1)
acosx+bsinx=c (B2)
PRET процедурасына В1 неВ2 теңдеулерін (мақсаттарын) таңдау негізге алынып,мынадай үш қадамнан тұратын әрекеттер тізбегі басшылыққа алынған:
1.Егер мүмкін болса,міндетті ережелерді пайдалану.
2.Ол мүмкін болса,сәйкес түрде таңдалған міндетті емес ережені пайдалану.
3.Программаға енгізілген өрнектер жиынынан ең қолайлы өрнекті таңдап,бірінші қадамға қайтып оралу.
Төменде тригонометрия бойынша прораммаға енгізілген ережелер көрсетілген
Міндетті емес шығару ережелері (МЕЕ)
2.1-кесте
| № | Өрнек |
Алмастырылатын өрнек |
| 1 | Sin2x | 2sinxcosx |
| Cos2x | 2cos2x-1 | |
| 2 | Sinusinv | 1/2(cos(u-v)-cos(u+v)) |
| Cosucosv | 1/2(cos(u-v)+cos(u+v)) | |
| 3 | Sin2x | 1-cos2x |
| Sinxcosx | 1/2sin2x | |
| 4 | Sin2v | 1/2 (1-cos2v) |
| Cos3v | 1/2 (cos3v+ cos3v) | |
| 5 | Tg v | Sinv/cos |
| 6 | Sinv/cosv | Tgv |
| 7 | Cos3v | 1/4(cos3v+ cos3v) |
| 8 | Cos2v | 1/(1+tg2v) |
| 9 | Trigo(u+v) | F(trigou, trigouv) |
Мұндағы trigo,trigov кері тргонометриалық функцияларды білдіреді.
Ережелердің кейбірі шешу бағытын қиныдатып жіберуіде мүмкін (мысалы, екінші ереже), не сан жағынан көбейтіліп кетуі, сапасыздануы ықтимал (мысалы,2, 4- ережелер).Ережелер барлық мүмкін болған жағдайларда қолданыла береді.
Міндетті шығару ережелері. (МЕ)
| № | өрнек | Түрлендірілген түрі | Іс-әрекет |
| (a+b)n | Қосындыға айналдыру | Көшіріп жазу | |
| A=c2 | Радикалдан құтылу | ||
| Sinu+sinv | 2sin | Көбейтіндіге түрлену | |
| An-b | (a-b)*<полином> | Көбейтінділерге жіктеу | |
| Ctg | 1/tgx | Түрлендіру | |
| Tgx | Sinx/cosx | Түрлендіру | |
| U(x) | U(x+p/4) | Егер u өрнегі синус пен косинусқа симметриялы болса,х-ті x+p/ | |
| 8 | 1)Егер өрнекте синус және косинус тек жұп дәрежеде кездессе,оны P(tgx)=0 өрнегіне түрлендіру үшін sin2x1-cos2x ережесін пайдалану.
2)Егер олар тек тақ дәрежеде кездессе,өрнекті cos2x функциясына бөліп, өрнекті P(tgx)=0 не (cosx)=0 түріне түрлендіру. |
||
| 9 | Егер теңдеуде бөлшек енгізілген мүше бар болса,оны ортақ бөлімге келтіру. | ||
PRET процедурасы теңдеу шешімін ағаш бұтақтары сияқты ирархиялық түрде іздейді.Теңдеу жоғарыда көрсетілген ережелер бойынша түрлендіріп,жеңілдетілген ішкі теңдеулерге айналдырылады да, олар жеке шешіледі.