函數(shù)微分、差分差商及連分數(shù)的Mizar實現(xiàn)研究.pdf

1、青島科技大學碩士學位論文函數(shù)微分、差分差商及連分數(shù)的Mizar實現(xiàn)研究姓名：張燕申請學位級別：碩士專業(yè)：應用數(shù)學指導教師：李博20070530函數(shù)微分、差分籌商及迕分數(shù)的Mizar實現(xiàn)研究THEFUNCTIONDIFFERENTIAL，DIFFERENCE，DIFFERENCEQUOTIENTANDCONTrNUEDFRACTl0NINMIZARABSTRACTTheprojectMizariscreatedanddevelopswit

2、hthedevelopmentofautomatedtheoremprovingwhichisabranchofartificialintelligenceMizarisaproofcheckerwhichisusedinbuildingMizarMathematicalLibraryMi7mrprojectisundertheleadershipofAndrzejTrybulecatthePlockScientificSocietyP

3、olandTheoriginalMizarisdesignedtohelpmathematicianswritemathematicalpaperanditbaseontheJagkowskistyleofnaturaldeductionTodayMizarhasbecomeafoITnalizationofmathematicalknowledge，withthefunctionofproving，veilfringandtypese

4、ttingMizarhasalargeMizarMathematicalLibraryembodyingmorethan960articleswfiRenbyprofessorsfromPoland，Japan，China，CanadaMMLalmostcontainsallbranchesofmathematicsEspeciallyinthefofinalizationofcontinuouslatticestheoremJorda

5、n’scurvetheoremandBrouwerfixedpointtheorem，MizarhasagreatadvantageThjsdissertationdescfibesthehistoryoftheoremautomaticproofandMizarsystemandhowtowritearticlesinMizarsystemThemainworkofthepaperissummarizedastbllowing：1、1

6、11eautomatedreasoningandverificationdifierentialsforsomespecialcompositefunctionsisimplementedinMizarsystem2、ForthefirsttimethefunctorshiftfDbDandcDaredefinedinMizarBasedonthedefinitionsofthem，theinfinitefunctiondifferen

7、cesequencesforward—difference，backwarddiffereneeandcentral—differencearedefinedandtheconnectionofthemispresentedandimplementedjnMizar3、Forthefirsttimethecontinuedfractionformofarealnumberandtheconvergencefractionaredefin

8、edandthepropeOyofthemisverifiedinMizarTheautomaticreasoningmadprovingprocesswhichisrelatedtotheaboveaspects，havebeencompletedandverifiedtobecorrectinMizarsystemKEYWORDS：Mizarautomatedtheoremproving，differential，differenc