| In the past, researchers mostly focused on the circumscriptive theory. In1994, Liftchitz also proposed the circumscriptive theory which can due with func-tions. In recent years, there are a large number of Scholars concerned aboutfunctions, various functional semantics have been proposed, but the study forCircumscriptive theory with functions is less and no solver for circumscriptivetheory with functions.This paper proposes a method by introducing auxiliary verb remove func-tions, not only keep the original meaning of functions, and provides the basis forthe circumscriptive theory of equivalent translation, which gets rid of first orderformula of functions embed the qualified in the stable model semantics, and thenconverted to disjunction logic programs.The solution of problem can be got atlast. The meaning of the thesis work basically has two points as follows:Firstly, on the theoretical study which focuses on duing with functions ofcircumscriptive theory, for functions Cancellation without losing its semantic,successful translation with first-order circumscriptive theory from functions tothe first-order stable model semantics theory. The method compared with theprevious studies, focused on the first-order logic, with function solution of thefirst-order logic enhances the description, and circumscriptive theory is mainlyfocused on looking for the smallest models, It also expands the research scopeof circumscriptive theory and strengthens the flexibility in the circumscriptivetheory on nonmonotone logic reasoning, which enlarge research domain in themonotonic reasoning theory is extremely meaningful.Secondly, In the application, due to the success of handling functions, which expands the application range of circumscriptive theory in the real world. Atthe same time, combined with the advantages of computing complexity circum-scriptive theory and the smallest model of the problem,which broadens the ideasabout Circumscriptive theory. |
PDF Full Text Request