| Default logic was proposed by Reiter as a viable paradigm for nonmonotonic reasoning. The premise behind default logic is that people tend to believe things by default, or in absence of the evidence to the contrary. In this manner, information that is not explicitly stated can be inferred from a default theory.; Despite the powerful nature of default logic, it has not been used extensively as a logic programming paradigm. Two primary causes for this have been identified. The first is that there is no general top-down proof procedure for default logic. Thus, although default logic may give us intuitively correct results, there is no easy way to compute them. The second is that default logic is not well understood in terms of contemporary non-monotonic reasoning paradigms, such as the well-founded semantics or the stationary semantics, preventing default logic from being identified with the current science of logic programming. This thesis is an attempt to alleviate these problems.; First, default logic is related to the well-founded semantics. More specifically, it is shown that a logic program P can be translated, via a syntactic translation, into a default theory {dollar}Pi{dollar}, such that {dollar}Pi{dollar} has a single extension corresponding to the well-founded model of P. Thus, default logic can be used to represent the well-founded semantics. The possibility that default logic can be used to represent the stationary semantics is also discussed. Hence, default logic is shown to be an integral part of contemporary logic programming.; Once default logic has been given this broader representational power, a top-down proof procedure is developed. The proof procedure has several nice properties. It is valid for a larger class of default theories than any other proof procedure previously developed for default logic, encompassing normal default theories, stratifiable default theories, and many semi-normal default theories. Further, the procedure does not necessarily have to look at all defaults in order to develop a proof, giving it the potential to be more efficient than a bottom up approach. Finally, the procedure returns a subset of the entire extension, making future queries more efficient. |
