【幾何定理機器證明與例證法】杭州大學.pdf

摘要东一章.几但实理机口飞明丽墓本荒理.一— 51几何定理杞明的机械化与Hilbentn械化定理 S1.无序几何的机械您定理 1.有序n但的机械化定理基二章,用例记法飞明平面n何定理 §2.!几何问题代sr5r何问题类.几但命题分能树、.了消元法 2.

n0 4 若一章几何定理机四证明的基本虎理机化定理证明的思想日以追朔到十七世纽aLeibni子.到了本世纪由于Hilbert及其在数理逻辑方面的跟随者的工作.而精确地学化了:机楼代这个问题实质上是用计标量血复杂性代替质丽团难.这种计称量丽复杂性以前是人能力作能达到的,但是自从有了计标机及其飞遮发展.已经变得很乎凡了。在初甘几何方面已经有很多机械化宝理.对于确实日以过行机械化你明的凭理,我们提出三种不同类型.它们日困三种机械化方法来征明.将分别在下面几节讨论.苗生一步是几向问题代数化.把几何空理作明化为一些代数关系式的处理问题.

n06 就效率而言,工最高,直决之,黑则效率颇低,选今为此.迎没据之证卧非平凡四定星.机 S1.几但定理记明的械化与Hbrt机械化定理定义1.如果在几何G中一个有意义的几但语句(S),在附加了若干个在几但中有意义的条伴为附加假设后能够成立.则棘这个语句心是一一个有条件的空理.或定理(s)nericaly 成立附如的条体称为使空理成立的非退化条件,宝义2.对于一个社ricaly成立的生理(s 如果有一个过程从(S)的假投却分出发.依几何白中的公理及逻辑推理法则逐步进行.