| Knowledge Representation and Reasoning(KRR)is a main research branch of artificial intelligence,and it provides a theoretical and technical foundation for knowledge formalization and problem solving of knowledge-based systems.To handle different kinds of knowledge and implement knowledge-based problem solving,powerful knowledge representation languages and corresponding general solving techniques become long-term research tasks of KRR.As a main method of KRR,logic programming has been greatly advanced over decades.Particularly,different kinds of logic programming languages have been presented,such as Prolog,Answer Set Programming(ASP),P-log,Prob Log,Markov Logic Networks(MLN)etc.Among the languages,logic programming under the answer set semantics and Markov Logic Networks(LPMLN)is a new logic formalism that combines the non-monotonic reasoning ability of ASP and the probabilistic inference ability of MLN.For the expressivity of LPMLN,it provides a new method to handle uncertain,inconsistent,and non-monotonic knowledge.Therefore,it has been applied to many problems such as visual objects classification and question answering etc.For the solving techniques of LPMLN,existing LPMLNsolvers translate an LPMLNprogram into other logic formalisms such as ASP and MLN,and compute the inference results via ASP and MLN solvers,which support the preliminary applications of LPMLN.However,there are no theoretical results for optimization approaches to solving LPMLN,which makes the existing LPMLNsolvers inefficient and prevents the applications of LPMLN.For the development of LPMLNsolving techniques and the efficiency of LPMLNsolvers,theories and algorithms w.r.t.solving parallelization,solving simplification,and programs simplification of LPMLNare studied,and programs partition and simplification related theories and techniques are presented.The main contributions of the dissertation are as follows.(1)To support the parallelization of LPMLNsolving,based on the partition of solving spaces of LPMLN,the augmented subsets theorem for LPMLNis proven,and the augmented subsets based partition and parallel method to solve LPMLNprograms are presented.According to the semantics of LPMLN,the notions and semantics of augmented subsets are presented,and the augmented subsets theorem of LPMLNis proven.Based on the semantics of augmented subsets,an ASP based approach to solving augmented subsets is presented.Based on the augmented subsets theorem and the solving approach to augmented subsets,a parallel algorithm to solve LP(MLN program is presented.(2)To support the parallelization and simplification of LPMLNsolving,based on the partition of solving procedures of LPMLN,the splitting set theorem for LPMLNis proven, and the splitting set based partition method,parallel methods,and simplifications to solve LPMLNprograms are presented.According to the dependency of literals in an LPMLNprogram,the notions of splitting sets for LPMLNare presented,and the splitting set theorem for LPMLNis proven.Based on the splitting set theorem, simplification and parallel approaches to solving LPMLNprograms are presented.(3)To verify the efficiency of augmented subsets and splitting sets based parallelization approaches,a set of test cases of LPMLNis proposed.Based on the test cases,the experiments for the parallelization approaches are carried out.The experimental results show the parallelization approaches can improve the efficiency of LPMLNsolving. Furthermore,several real-world applications of the parallelization approaches based solver of LPMLNare presented,such as the logical reasoning applications in 863 program“key technology and systems of knowledge linking,reasoning,and retrieve in open domain”etc.(4)To reduce the rules or literals of an LPMLNprogram under semantics equivalences, the results of strong equivalences for LPMLNare presented,and a strong equivalence based simplification methods of LPMLNprograms is presented.Based on the ordinary equivalences of LPMLN,the notions of semi-strong,w-strong,and p-strong equivalences are presented.Based on the models of logic of Here-and-There(HT- models),characterizations of strong equivalences of LPMLNare presented.And the computational complexity of deciding strong equivalences of LPMLNis proven to be co-NP-complete.Based on the above results,the strong equivalences based programs simplification can reduce the searching spaces of LPMLNsolving and improve the efficiency of LPMLNsolving.However,the simplification has high computational complexity.(5)To decide the semi-strong equivalence efficiently,a fully automatic approach to searching the syntactic conditions deciding strong equivalences(SE-condition)amon LPMLNprograms is presented.To study the general forms of SE-conditions,the notions of independent sets and S-*transformations of logic programs are presented. And the strong equivalences and non-strong equivalences preserving properties of S-*transformations are proven.Based on these properties,an algorithm to find SE-conditions of LPMLNprograms is presented.Via the algorithm,some SE-conditions of LPMLNare reported.The results presented in this dissertation help us to implement a better solver of LPMLN,and it would bring more understanding for the studying of LPMLNand other logic formalisms. |
PDF Full Text Request