[几何定理机器证明与例证法]杭州大学

【幾何定理機器證明與例證法】杭州大學.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)的假投却分出发.依几何 白中的公理及逻辑推理法则逐步进行.
———— 文字由OCR识别(未校验)，可能存在错字；请以原始完整版为准。