基于邏輯的自動(dòng)推理研究.pdf

1、自動(dòng)推理是一門(mén)在給定知識(shí)及有關(guān)推理策略的前提下,研究用計(jì)算機(jī)幫助人們進(jìn)行推理的學(xué)科.多種類(lèi)邏輯及多種類(lèi)謂詞演算是經(jīng)典一階邏輯及其演算的重要拓展,并已經(jīng)在計(jì)算機(jī)科學(xué)的諸多領(lǐng)域得到了廣泛運(yùn)用,如知識(shí)表示、程序設(shè)計(jì)語(yǔ)言、軟件規(guī)約與驗(yàn)證等.與基于歸結(jié)原理的經(jīng)典謂詞演算相比,多種類(lèi)謂詞演算具有更高的演繹效率.為進(jìn)一步提高演繹效率與簡(jiǎn)化計(jì)算機(jī)程序設(shè)計(jì)結(jié)構(gòu),提出了一種基于歸結(jié)原理的多種類(lèi)謂詞演算的演繹策略,即RLD(Rightmost Linear

2、Deduction)演繹,并證明了它的完備性.實(shí)現(xiàn)了基于RLD演繹的多種類(lèi)謂詞演算的一個(gè)原型系統(tǒng)并成功求解了著名的人工智能問(wèn)題,即Steamroller問(wèn)題.為了在模糊邏輯中集成相似性關(guān)系并考慮其近似推理,把相似性關(guān)系看成是一種模糊相等關(guān)系,提出了一種帶有相似性關(guān)系的模糊邏輯,給出了帶有相似性關(guān)系的模糊邏輯的語(yǔ)法及語(yǔ)義結(jié)構(gòu).調(diào)解規(guī)則是在帶有相等關(guān)系的經(jīng)典謂詞演算中提出的推理規(guī)則,它能夠進(jìn)行高效的等值推理.將調(diào)解規(guī)則拓展到了帶有相似性關(guān)系

3、的模糊邏輯謂詞演算,討論了基于歸結(jié)與調(diào)解規(guī)則的近似推理.給出并證明了基于歸結(jié)與調(diào)解方法的近似推理的有關(guān)屬性,證明了如果子句集S中的每一個(gè)子句的真值都大于0.5,那么從S中使用歸結(jié)與(或)調(diào)解規(guī)則推出的任意一個(gè)邏輯結(jié)果均是有效的.考慮到許多自動(dòng)推理和問(wèn)題解決系統(tǒng)均是基于否證法,證明了基于歸結(jié)與調(diào)解規(guī)則對(duì)模糊謂詞演算的完備性定理.自動(dòng)推理系統(tǒng)的性能測(cè)試與評(píng)價(jià)是自動(dòng)推理領(lǐng)域備受關(guān)注的問(wèn)題.為進(jìn)行公正的系統(tǒng)評(píng)價(jià),需要一系列的評(píng)價(jià)標(biāo)準(zhǔn)以便測(cè)試者做

4、出合理、準(zhǔn)確、公正的評(píng)價(jià)結(jié)論.其中,問(wèn)題的表示是其中主要原則之一.為了給自動(dòng)推理領(lǐng)域提供一個(gè)統(tǒng)一的問(wèn)題表示格式,提出了一個(gè)基于多種類(lèi)邏輯的知識(shí)標(biāo)記語(yǔ)言MSKML(Many-Sorted KnowledgeMarkup Language).使自動(dòng)推理成為一種Web服務(wù),既可以為Web用戶(hù)提供自動(dòng)推理服務(wù),也可以使Web用戶(hù)參與自動(dòng)推理系統(tǒng)的測(cè)試工作,從而獲得更豐富的實(shí)驗(yàn)數(shù)據(jù)以便做出更為公正合理的系統(tǒng)評(píng)價(jià).為了給Web用戶(hù)提供自動(dòng)推理Web