Lattice-Valued Logical System And Automated Reasoning Based On Lattice Implication Algebra

The research ofnon－classical lope has always been a very attractive dlrec－ non of Artificial Intelligence．In recent years,theory and technology of automated theorenlprovinghased on non－classlcalloglcs are developingrapldlyand many automated theorem provers have been tised successfully In matllelnatlcs,engineer－ lug and other areas．Used Previous Internal and external outcome ofresearches In these direction for reference。the allthor stlldled the properties oflattlce Inl－ l)licatlon algebra and lattice－vallled logical systelll wltll trllth－valllesfield belllg a lattice lmpllcatlon algebra,andon the base ofwhich,the authordlscussed In de－ tails about the lattice－valued resolution principle oflattlce－valued logical system． The specific contents are s follows: Part One The Study of Lattice Implication Algebra On the basis of previous results of lattice implication algebra．the part(:on－ sists of＊theili＊lliereallwffollilli＊＊【＾,000taltal＊ fOllowingthree points: l．A lllethod ofconlputingthe colllplelllentary elemellt ofally one In alattlce implication algebra was discussed In details and a practicable approach was given． 2．The theorem was shown that lattice lmpllcatlon algebra can not be con－ Stl·lit:tAtl Off CAlt3lll SI＞eC181 dlstl'lhlltlV618tt1Ces；Sllf:h s《5．心6,心7,令8 3lidO8＋k． 3．The structural feature ofnon－chain－type and non－Boolean－algebratype lattice lmpllcatlon algebra was discussed and the result that ifa lattice implication algebrahas alld only has onedual atom then It Is a chain was proved． Part Two The Study of ReResolution Principle in L8ttice－v古ined Logic based on Lattice Implication Algebra Ill this P8ft；th6 3llthof d！SCilSS6d th6 f6SOI［ltlOll－b8S6d Ih6thod Of slltoinst6d f6Anolllllg．ThiS psft COliSIStS Ofth6 follOWlllg poilltS: 1．The semantical andsyntactlcalfeatures ofresolutlon－basedautomated reasoningln classical logic was analyzed．The difference on resolution－basediv Jgmethod between the classical logic and lattice-valued logic was discussed in details.2. A algebraical method about resolution-based automated reasoning in classical logic was given. That method translated the decidability of satisfiability of logical formula into the decidability of solution of congruence equation array.3. The resolution-based automated reasoning method of simple and complicate clause sets in LP(X) was discussed in details. The concept of resolution on filter was given and a practicable approach was attained. The soundness and weak completeness theorem of that method was proved.4. The concept and method of resolution on filter in lattice- valued first-order logic SLF(X] was discussed and the concepts and properties of Skolemlzation and Herbrand field in it was discussed too.5. The concept of constrained resolution was give after the analyzing of resolution-based method of classical logic in lattice-valued logic.Part Three The Study of Lattice- Valued Logical SystemIn this part, the author constructed a lattice- valued prepositional logical system Jz?,,p with the truth-field of it is a lattice implication algebra. This part consists of the following points:1 . The concepts and properties of (a, /3)-semantical implication were discussed; the concepts and condition of keeping (a, /3)-rule of lattice- valued logical formula were given too.2. The condition of choosing axioms and inference rule in ^fvp was analyzed.3. The concepts of proof under valuation and its properties were given. The soundness and weak deduction theorems were proved.4. The concepts of consistency of lattice-valued logical formula under valuation was given and the consistent theorem of it was proved also.