反證法在自動(dòng)推理系統(tǒng)中的研究與實(shí)現(xiàn).pdf

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

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

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