Search

This paper contributes to the development of theoretical foundations of answer set programming. Groundbreaking work on the SM operator by Ferraris, Lee, and Lifschitz proposed a definition/semantics for logic (answer set) programs based on a syntactic transformation similar to parallel circumscription. That definition radically differed from its predecessors by using classical (second-order) logic and avoiding reference to either grounding or fixpoints. Yet, the work lacked the formalization of crucial and commonly used answer set programming language constructs called aggregates. In this paper, we present a characterization of logic programs with aggregates based on a many-sorted generalization of the SM operator. This characterization introduces new function symbols for aggregate operations and aggregate elements, whose meaning can be fixed by adding appropriate axioms to the result of the SM transformation. We prove that our characterization coincides with the ASP-Core-2 semantics for logic programs and, if we allow non-positive recursion through aggregates, it coincides with the semantics of the answer set solver CLINGO. [ABSTRACT FROM AUTHOR]

In this work we design an information extraction tool text2alm capable of narrative understanding with a focus on action verbs. This tool uses an action language ALM to perform inferences on complex interactions of events described in narratives. The methodology used to implement the text2alm system was originally outlined by Lierler, Inclezan, and Gelfond (In IWCS 2017 – 12th International Conference on Computational Semantics – Short Papers (2017)) via a manual process of converting a narrative to an ALM model. We refine that theoretical methodology and utilize it in design of the text2alm system. This system relies on a conglomeration of resources and techniques from two distinct fields of artificial intelligence, namely, (i) knowledge representation and reasoning and (ii) natural language processing. The effectiveness of system text2alm is measured by its ability to correctly answer questions from the bAbI tasks published by Facebook Research in 2015. This tool matched or exceeded the performance of state-of-the-art machine learning methods in six of the seven tested tasks. We also illustrate that the text2alm approach generalizes to a broader spectrum of narratives. On the path to creating system text2alm, a semantic role labeler text2drs was designed. Its unique feature is the use of the elements of the fine grained linguistic ontology VerbNet as semantic roles/labels in annotating considered text. This paper provides an accurate account on the details behind the text2alm and text2drs systems. [ABSTRACT FROM AUTHOR]

Answer set programming is a declarative logic programming paradigm geared towards solving difficult combinatorial search problems. While different logic programs can encode the same problem, their performance may vary significantly. It is not always easy to identify which version of the program performs the best. We present the system predictor (and its algorithmic backend) for estimating the grounding size of programs, a metric that can influence a performance of a system processing a program. We evaluate the impact of predictor when used as a guide for rewritings produced by the answer set programming rewriting tools projector and lpopt. The results demonstrate potential to this approach. [ABSTRACT FROM AUTHOR]

Search-optimization problems are plentiful in scientific and engineering domains. Artificial intelligence (AI) has long contributed to the development of search algorithms and declarative programming languages geared toward solving and modeling search-optimization problems. Automated reasoning and knowledge representation are the subfields of AI that are particularly vested in these developments. Many popular automated reasoning paradigms provide users with languages supporting optimization statements. Recall integer linear programming, MaxSAT, optimization satisfiability modulo theory, (constraint) answer set programming. These paradigms vary significantly in their languages in ways they express quality conditions on computed solutions. Here we propose a unifying framework of so-called extended weight systems that eliminates syntactic distinctions between paradigms. They allow us to see essential similarities and differences between optimization statements provided by distinct automated reasoning languages. We also study formal properties of the proposed systems that immediately translate into formal properties of paradigms that can be captured within our framework. [ABSTRACT FROM AUTHOR]

Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. CASP demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt2smt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Traveling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP. [ABSTRACT FROM AUTHOR]

Answer set programming is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing different knowledge representation formalisms. Frequently, several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper presents formal results carefully relating a number of interesting program rewritings. It also provides the proof of correctness of system projector concerned with automatic program rewritings for the sake of efficiency. [ABSTRACT FROM AUTHOR]

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. [ABSTRACT FROM AUTHOR]

Researchers in answer set programming and constraint programming have spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming. Constraint answer set programming languages and systems proved to be successful at providing declarative, yet efficient solutions to problems involving hybrid reasoning tasks. One of the main contributions of this paper is the first comprehensive account of the constraint answer set language and solver ezcsp, a mainstream representative of this research area that has been used in various successful applications. We also develop an extension of the transition systems proposed by Nieuwenhuis et al. in 2006 to capture Boolean satisfiability solvers. We use this extension to describe the ezcsp algorithm and prove formal claims about it. The design and algorithmic details behind ezcsp clearly demonstrate that the development of the hybrid systems of this kind is challenging. Many questions arise when one faces various design choices in an attempt to maximize system's benefits. One of the key decisions that a developer of a hybrid solver makes is settling on a particular integration schema within its implementation. Thus, another important contribution of this paper is a thorough case study based on ezcsp, focused on the various integration schemas that it provides. [ABSTRACT FROM PUBLISHER]

Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will boost the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction, we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs. [ABSTRACT FROM PUBLISHER]

Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many answer set programs. We also introduce conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. We show how the notion of a conservative extension can be used to justify the common projection rewriting. [ABSTRACT FROM AUTHOR]

Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is ΣP2-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely dlv, gnt, cmodels, clasp and wasp. In this paper, we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers dlv, gnt, and cmodels. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers. [ABSTRACT FROM PUBLISHER]

Nonmonotonic causal logic, introduced by McCain and Turner (McCain, N. and Turner, H. 1997. Causal theories of action and change. In Proceedings of National Conference on Artificial Intelligence (AAAI), Stanford, CA, 460–465) became the basis for the semantics of several expressive action languages. McCain's embedding of definite propositional causal theories into logic programming paved the way to the use of answer set solvers for answering queries about actions described in such languages. In this paper we extend this embedding to nondefinite theories and to the first-order causal logic. [ABSTRACT FROM AUTHOR]

Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53–65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53–87). Like an HCF program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body. [ABSTRACT FROM AUTHOR]

A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as “satisfiability modulo answer-set programming,” where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID). [ABSTRACT FROM AUTHOR]

Nieuwenhuis et al. (2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937977 showed how to describe enhancements of the Davis–Putnam–Logemann–Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for several algorithms that generate answer sets for logic programs: smodels, smodelscc, asp-sat with Learning (cmodels), and a newly designed and implemented algorithm sup. This approach to describe answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems. [ABSTRACT FROM AUTHOR]