The Research For The Well-founded Semantics Of Disjunctive Logic Programs With Functions

In the 1980 s, the logic programming language has made breakthrough progress on the descriptive semantic, which was stable model semantics(also called answer set semantics), and it opened the door to the research of logic programs. There, a problem could be encoded as the logic programs, and an answer set of the logic programs is a feasible solution to the problem. Around the year of 2000, a variety of effective logic programming solver has been developed, and promote the application of logic programming language, and make answer set programming into a new level.However, lacking of functions for answer set programming in previous studies on logic program, so some experts and scholars have put forward the solving method of logic programs with functions at home and abroad in recent years, and the way of calculating stable model was formulating its completion and loop formulas. And they also has put forward the method to eliminate functions, as a new repeating replace each function, and add new function of atoms in to the corresponding rules to eliminate them. But it is difficult to determine whether a model is minimal, because checking a set of atoms is an answer set or not is difficult(∑2-complete).The well-founded semantics of normal logic programs is a hot spot in recent decade, since it can simplify the programs when calculating answer sets. So based on the theory proposed by Wang etc., we extend the well-founded semantics to disjunctive-free logic programs with functions, and we found this method could be able to solve the model of disjunctive logic programs with functions. The work in the paper:(1) we put forward a notion of unfounded set for the disjunctive logic programming with functions, proving its relations corresponding with stable model;(2) we study its well-founded semantics, and proves that it is the stable model when the well-founded model is total;(3) according to the above conclusion we design a stable model algorithm based on the SAT, to show a model of logic programs is a stable one of it and this isn’t satisfied under the condition of corresponded propositional formula, which theoretically provides an efficient approach to compute answer sets of disjunctive logic programs with functions.Finally, we use ASP to solve the Hamiltonian cycle problem, and research the existence, nonexistence, and hardness of evaluating Hamiltonian circuits in random graphs, and this also shows that ASP is very effective for declarative problem solving.