1、從50年代Tarski發(fā)表的《初等代數(shù)與初等幾何的判定問題》<'[25]>開始,到70年代的吳法<'[4,5]>,90年代的消點法<'[8,10]>,幾何定理機器證明的研究經(jīng)歷了幾個階段的發(fā)展.計算機技術(shù)的發(fā)展及可讀機器證明的出現(xiàn)<'[3,4]>,使這個方向的研究成果進入了實用階段.以張景中院士為領(lǐng)導(dǎo)的小組在此基礎(chǔ)上開發(fā)了一系列的智能教育軟件<'[10]>.得到廣大中小學教師,學生的歡迎.這些軟件最突出的一個特點就是自動推理.要讓計算機

2、能夠自動進行推理.首先要"教會"計算機推理的方法,計算機"掌握"了方法后,才能進行推理.因此,"教會"計算機推理方法是首要的.現(xiàn)行的推理軟件都是采用了前推搜索的推理模式.從題目的已知條件出發(fā),利用規(guī)則進行推理直至推出所需要的結(jié)論.在數(shù)學證明方法上屬于直接證明方法.這種方法只能證明一些肯定性的命題.但對于一些否定性,唯一性的命題采用直接證法不易證明,這就需要利用數(shù)學證明中的間接證明方法來證明.間接證明方法中比較常見的一種方法是反證法.盡管

3、幾何定理機器證明的研究在七十年代已經(jīng)取得突破,可讀證明的實現(xiàn)也近十年了.但自動推理在反證法方面還存在很大的不足.除了在《平面幾何》<'[22]>中見到有間接證法中的同一法外,其他的教育軟件中很少有實現(xiàn)反證法的.該文的工作就是向這個方向努力的一個嘗試,把數(shù)學證明中的反證法與機器證明中的前推搜索法相結(jié)合.使計算機在自動推理方面能夠更加完善.該文共分為四章:第一章,簡要介紹自動推理的歷史和發(fā)展,闡述該文要解決的問題.第二章,介紹該文的工作原理