Zautomatyzowanie dowodzenia twierdze\u0144 matematycznych poprzez przeniesienie pracy zwi\u0105zanej z procesem decyzyjnym na komputer, wykszta\u0142ci\u0142o swoj\u0105 w\u0142asn\u0105 metodologi\u0119 na styku informatyki, filozofii i matematyki. Najbardziej znanym tego typu przypadkiem jest dow\u00f3d twierdzenia o czterech barwach, podczas kt\u00f3rego do procesu dowodzenia wykorzystano komputer.<\/p>\n
Jak obszerny mo\u017ce by\u0107 taki dow\u00f3d? Jakie musi spe\u0142nia\u0107 warunki formalne, aby zosta\u0142 przyj\u0119ty w renomowanym czasopi\u015bmie jako dow\u00f3d matematyczny? Czy powinien by\u0107 zrozumia\u0142y dla naukowca nieb\u0119d\u0105cego specjalist\u0105 w danej dziedzinie? A mo\u017ce ograniczeniem powinna by\u0107 moc obliczeniowa komputera, na kt\u00f3rym zosta\u0142 uzyskany? Zapewne odpowiedzi na powy\u017csze pytania straci\u0142yby na znaczeniu, je\u017celi otrzymany dow\u00f3d komputerowy by\u0142by jedynym znanym lub odznacza\u0142 si\u0119 wi\u0119ksz\u0105 elementarno\u015bci\u0105 od klasycznego uzasadnienia b\u0105d\u017a naprowadza\u0142by na oryginaln\u0105 uniwersaln\u0105 metod\u0119. Czym jest zatem automatyczne dowodzenie twierdze\u0144 (ADT), jak nie rygorystycznym stosowaniem regu\u0142 wnioskowania, z t\u0105 tylko r\u00f3\u017cnic\u0105, \u017ce wykonywanym przez komputer? W obr\u0119bie rozleg\u0142ych, z\u0142o\u017conych teorii stosowanie ADT mo\u017ce s\u0142u\u017cy\u0107 do korekty rozbudowanych rozumowa\u0144, otrzymywania alternatywnych dowod\u00f3w. Niestety na niekorzy\u015b\u0107 tego podej\u015bcia przemawia fakt, \u017ce wi\u0119kszo\u015b\u0107 tak otrzymywanych rozumowa\u0144 jest stosunkowo d\u0142u\u017csza od tych wykonywanych klasycznie.<\/p>\n
Celem referatu jest przedstawienie automatycznych dowod\u00f3w wybranych twierdze\u0144 z ksi\u0119gi VI \u201dElement\u00f3w\u201d Euklidesa oraz arytmetyki odcink\u00f3w opisanej w \u201dGeometrii\u201d Kartezjusza. Ponadto zostan\u0105 zaprezentowane mo\u017cliwo\u015bci i ograniczenia zastosowania jednej z metod ADT w geometrii elementarnej, jak\u0105 jest metoda pola, za pomoc\u0105 kt\u00f3rej otrzymano powy\u017csze przyk\u0142ady. Do uzyskania automatycznych dowod\u00f3w twierdze\u0144 wykorzystano \u015brodowisko WinGCLC, jedn\u0105 z implementacji przytoczonej metody. <\/p>\n","protected":false},"excerpt":{"rendered":"
Zautomatyzowanie dowodzenia twierdze\u0144 matematycznych poprzez przeniesienie pracy zwi\u0105zanej z procesem decyzyjnym na komputer, wykszta\u0142ci\u0142o swoj\u0105 w\u0142asn\u0105 metodologi\u0119 na styku informatyki, filozofii i matematyki. Najbardziej znanym tego typu przypadkiem jest dow\u00f3d twierdzenia o czterech barwach, podczas kt\u00f3rego do procesu dowodzenia wykorzystano … Czytaj dalej