The aim of this thesis is to develop faster method for stable model computation of non-stratified logic programs and study its efficiency. It focuses mainly on the stable model and weak well founded semantics of logic programs. We propose an approach to compute stable models by where we first transform the logic program using paraconsistent relational model, then we compute the weak-well founded model which is used to generate a set of models consisting of the true and unknown values, which are tested for stability. We perform some experiments to test the efficiency of our approach which incurs overhead to eliminate negative values against a Naïve method of stable model computation.

Solution of any search problem lies in its search space. A search is a systematic examination of candidate solutions of a search problem. In this thesis, we present a search heuristic that we can cr-smodels. cr-smodels prunes the search space to quickly reach to the solution of a problem. The idea is to pick an atom for branching , that lowers the growth rate of the linear recurrence and thuse, minimizes the remaining search space. Our goal in developing cr-smodels is to develop a search heuristic that is efficient on a wide range of problems. Then, we test cr-smodels over a wide range of randomly generated benchmarks. we observed that often randomly generated graphs with no Hamiltonian cycle were trivial to solve. Since, Hamiltonian cycle is an important benchmark problem, my other goal is to develop techniques that generate hard instances of graphs with no Hamiltonian cycle.

Knowledge about actions is an important part of commonsense knowledge studied in Artificial Intelligence. For decades, researchers have been developing methods for describing how actions affect states of the world and for automating reasoning about actions. In recent years, significant progress has been made. In particular, the frame problem has been solved using nonmonotonic knowledge representation formalisms, such as logic programming under the answer set semantics. New theories of causality have allowed us to express causal dependencies between fluents, which has proved essential for solving the ramification problem. It has been shown that reasoning about actions described by logic programs and causal theories can be automated using answer set programming. Action description languages are high level languages that allow us to represent knowledge about actions more concisely than when logic programs are used. Many action description languages have been described in the literature, including B, C, and C+. Reasoning about dynamic domains described in languages C and C+ can be performed automatically using the Causal Calculator (CCalc), which employs SAT solvers for search, and the systems coala and cplus2asp, which employ answer set solvers such as clingo. The dissertation addresses problems of three kinds. First, we study some mathematical properties of expressive action languages based on nonmonotonic causal logic that were not well understood until now. This includes causal rules expressing synonymy, nondefinite causal rules, and nonpropositional causal rules. We generalize existing translations from nonmonotonic causal theories to logic programming under the answer set semantics. This makes it possible to automate reasoning with a wider class of causal theories by calling answer set solvers. Second, we design and study a new action language BC, which is more expressive in some ways than the existing and previously proposed languages. We develop a framework that combines the most useful expressive features of the languages B and C+, and use program completion to characterize the effects of actions described in these languages. Third, we illustrate the possibilities of the new action language by two practical applications: to the dynamic domain of the Reactive Control System of the space shuttle, and to the task planning of mobile robots. / text

abstract: Answer Set Programming (ASP) is one of the most prominent and successful knowledge representation paradigms. The success of ASP is due to its expressive non-monotonic modeling language and its efficient computational methods originating from building propositional satisfiability solvers. The wide adoption of ASP has motivated several extensions to its modeling language in order to enhance expressivity, such as incorporating aggregates and interfaces with ontologies. Also, in order to overcome the grounding bottleneck of computation in ASP, there are increasing interests in integrating ASP with other computing paradigms, such as Constraint Programming (CP) and Satisfiability Modulo Theories (SMT). Due to the non-monotonic nature of the ASP semantics, such enhancements turned out to be non-trivial and the existing extensions are not fully satisfactory. We observe that one main reason for the difficulties rooted in the propositional semantics of ASP, which is limited in handling first-order constructs (such as aggregates and ontologies) and functions (such as constraint variables in CP and SMT) in natural ways. This dissertation presents a unifying view on these extensions by viewing them as instances of formulas with generalized quantifiers and intensional functions. We extend the first-order stable model semantics by by Ferraris, Lee, and Lifschitz to allow generalized quantifiers, which cover aggregate, DL-atoms, constraints and SMT theory atoms as special cases. Using this unifying framework, we study and relate different extensions of ASP. We also present a tight integration of ASP with SMT, based on which we enhance action language C+ to handle reasoning about continuous changes. Our framework yields a systematic approach to study and extend non-monotonic languages. / Dissertation/Thesis / Ph.D. Computer Science 2013