命題邏輯中子句集的分類研究.pdf

1、定理機(jī)器證明是通過(guò)計(jì)算機(jī)實(shí)現(xiàn)定理自動(dòng)證明。自上世紀(jì)五十年代以來(lái)定理自動(dòng)證明一直是計(jì)算機(jī)科學(xué)研究的熱點(diǎn)之一，在數(shù)學(xué)、硬件測(cè)試與驗(yàn)證、軟件生成與驗(yàn)證、協(xié)議驗(yàn)證、人工智能方面都得到了成功的應(yīng)用。其中檢測(cè)和刪除邏輯公式中的冗余子句是該方向廣泛研究的基本問(wèn)題?；谝延械难芯抗ぷ鳎疚膰@命題邏輯中子句和文字的相關(guān)知識(shí)，取得的主要研究結(jié)果如下:
　　1、將命題邏輯的子句集中文字劃分為三類，即有用文字、必需文字和無(wú)用文字，分別給出了三種文字的定

2、義，同時(shí)得到了相應(yīng)的等價(jià)描述方法，進(jìn)而得到了三種文字之間的相互關(guān)系。得到了子句集中的必需文字是非冗余文字，子句集中的無(wú)用文字是冗余文字。
　　2、基于子句集中文字的劃分，得到了有用文字、必需文字和無(wú)用文字的判別方法，借助子句集的可滿足性給出了三種文字與子句集的可滿足性的等價(jià)條件。給出了有用文字、必需文字和無(wú)用文字的判定定理并設(shè)計(jì)相應(yīng)算法。
　　3、研究了命題邏輯的子句集中冗余子句的性質(zhì)，得到了命題邏輯的子句集中冗余子句的等價(jià)