Decidability And Translatability Of Nonmonotonic Logics

One of the most difcult problems in the area of artifcial intelligence is how toprogram computers to solve problems with commonsense knowledge. Nonmonotoniclogics are an important class of knowledge representation formalisms targeting on thisproblem. In this dissertation, we devote ourselves to the decidability and translatabilityof frst-order nonmonotonic logics. Our main contributions are as follows:1. We carry out a comprehensive study in fnding decidable prefx-vocabularyclasses of frst-order language under the stable model semantics and circumscription.In detail, we identify six prefx-vocabulary classes which are maximally decidable un-der the semantics of circumscription, and one prefx-vocabulary class which is max-imally decidable under the stable model semantics. We also fnd a bunch of classeswhich are undecidable under either semantics. By these results, the boundaries of de-cidability and undecidability under these two semantics are almost clarifed.2. We make a thorough investigation in identifying the (in)translatability amongthe following languages: frst-order language under the stable model semantics, frst-order circumscription, universal second order logic, and three kinds of logic programs.We focus on four kinds of translatability which are classifed by allowing or not allow-ing auxiliary constants, and also classifed by considering fnite structures or arbitrarystructures. In the dissertation, we work out almost all the results about these four kindsof (in)translatability for all the above-mentioned languages. From these results, someinteresting conclusions can be drawn. For example, we fnd that there are a class ofproblems which can be represented by disjunctive logic programs but have no naturalencodings in disjunctive logic programs in some sense.3. We also study serval model-theoretical properties of logic programming andstable model semantics. In particular, we prove that disjunctive logic programs understable model semantics satisfy the downward L o¨wenheim-Skolem property, i.e., everydisjunctive logic program has a stable model if and only if it has a countable one. We also show that the real system can be represented in a frst-order theory under thestable model semantics. These results mean that the frst-order language under thestable model semantics is strictly more expressive than logic programming.4. Based on the results of translatability, we develop a prototype solver for frst-order theories under the stable model semantics over fnite structure. Two benchmarksare then proposed to verify the efectiveness of the solver. In addition, we also putforward to an efcient translation that converts frst-order circumscriptive theories intofrst-order theories under the stable model semantics, which paves a way to designsolvers for frst-order circumscription over fnite structures.