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

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

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