Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 27 of 27
Full-Text Articles in Physical Sciences and Mathematics
External Behavior Of A Logic Program And Verification Of Refactoring, Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, Nathan Temple
External Behavior Of A Logic Program And Verification Of Refactoring, Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, Nathan Temple
Computer Science Faculty Publications
Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.
System Predictor: Grounding Size Estimator For Logic Programs Under Answer Set Semantics, Daniel Bresnahan, Nicholas Hippen, Yuliya Lierler
System Predictor: Grounding Size Estimator For Logic Programs Under Answer Set Semantics, Daniel Bresnahan, Nicholas Hippen, Yuliya Lierler
Computer Science Faculty Publications
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 …
Positive Dependency Graphs Revisited, Jorge Fandinno, Vladimir Lifschitz
Positive Dependency Graphs Revisited, Jorge Fandinno, Vladimir Lifschitz
Computer Science Faculty Publications
Theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that concept and show that the new understanding of positive dependency makes it possible to strengthen some of these results.
What Is Answer Set Programming To Propositional Satisfiability, Yuliya Lierler
What Is Answer Set Programming To Propositional Satisfiability, Yuliya Lierler
Computer Science Faculty Publications
Propositional satisfiability (or satisfiability) and answer set programming are two closely related subareas of Artificial Intelligence that are used to model and solve difficult combinatorial search problems. Satisfiability solvers and answer set solvers are the software systems that find satisfying interpretations and answer sets for given propositional formulas and logic programs, respectively. These systems are closely related in their common design patterns. In satisfiability, a propositional formula is used to encode problem specifications in a way that its satisfying interpretations correspond to the solutions of the problem. To find solutions to a problem it is then sufficient to use a …
On Abstract Modular Inference Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński
On Abstract Modular Inference Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński
Computer Science Faculty Publications
Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience, and computational benefits. We introduce the concepts of abstract inference modules and abstract modular inference systems to study general principles behind the design and analysis of model generating programs, or solvers, for integrated multi-logic systems. We show how modules and modular systems give rise to transition graphs, which are a natural and convenient representation of solvers, an idea pioneered by the SAT community. These graphs lend themselves well to extensions that capture such important solver design features as learning. In the paper, we consider two …
Abstract Disjunctive Answer Set Solvers, Remi Brochenin, Yuliya Lierler, Marco Maratea
Abstract Disjunctive Answer Set Solvers, Remi Brochenin, Yuliya Lierler, Marco Maratea
Computer Science Faculty Proceedings & Presentations
A fundamental task in answer set programming is to compute answer sets of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has an answer set 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 and CLASP. 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. In particular, we present transition systems for CMODELS …
Abstract Modular Inference Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński
Abstract Modular Inference Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński
Computer Science Faculty Proceedings & Presentations
Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience and computational benefits. We introduce the concepts of abstract inference modules and abstract modular inference systems to study general principles behind the design and analysis of model-generating programs, or solvers, for integrated multilogic systems.We show how modules and modular systems give rise to transition graphs, which are a natural and convenient representation of solvers, an idea pioneered by the SAT community. We illustrate our approach by showing how it applies to answer-set programming and propositional logic, and to multi-logic systems based on these two formalisms.
Modular Answer Set Solving, Yuliya Lierler, Miroslaw Truszczyński
Modular Answer Set Solving, Yuliya Lierler, Miroslaw Truszczyński
Computer Science Faculty Proceedings & Presentations
Modularity is essential for modeling large-scale practical applications.We propose modular logic programs as a modular version of answer set programming and study the relationship of our formalism to an earlier concept of lp-modules.
Logic Programs Vs. First-Order Formulas In Textual Inference, Yuliya Lierler, Vladimir Lifschitz
Logic Programs Vs. First-Order Formulas In Textual Inference, Yuliya Lierler, Vladimir Lifschitz
Computer Science Faculty Proceedings & Presentations
In the problem of recognizing textual entailment, the goal is to decide, given a text and a hypothesis expressed in a natural language, whether a human reasoner would call the hypothesis a consequence of the text. One approach to this problem is to use a first-order reasoning tool to check whether the hypothesis can be derived from the text conjoined with relevant background knowledge, after expressing all of them by first-order formulas. Another possibility is to express the hypothesis, the text, and the background knowledge in a logic programming language, and use a logic programming system. We discuss the relation …
Towards A Tight Integration Of Syntactic Parsing With Semantic Disambiguation By Means Of Declarative Programming, Yuliya Lierler, Peter Schüller
Towards A Tight Integration Of Syntactic Parsing With Semantic Disambiguation By Means Of Declarative Programming, Yuliya Lierler, Peter Schüller
Computer Science Faculty Proceedings & Presentations
We propose and advocate the use of an advanced declarative programming paradigm – answer set programming – as a uniform platform for integrated approach towards syntax-semantic processing in natural language. We illustrate that (a) the parsing technology based on answer set programming implementation reaches performance sufficient for being a useful NLP tool, and (b) the proposed method for incorporating semantic information from FRAMENET into syntactic parsing may prove to be useful in allowing semantic-based disambiguation of syntactic structures.
Constraint Answer Set Programming, Yuliya Lierler
Constraint Answer Set Programming, Yuliya Lierler
Computer Science Faculty Publications
Constraint answer set programming (CASP) is a novel, promising direction of research whose roots go back to propositional satisfiability (SAT). SAT solvers are efficient tools for solving boolean constraint satisfaction problems that arise in different areas of computer science, including software and hardware verification. Some constraints are more naturally expressed by non-boolean constructs. Satisfiability modulo theories (SMT) extends boolean satisfiability by the integration of non-boolean symbols defined by a background theory in another formalism, such as a constraint processing language. Answer set programming (ASP) extends computational methods of SAT in yet another way, inspired by ideas from knowledge representation, logic …
Representing First-Order Causal Theories By Logic Programs, Paolo Ferrarris, Joohyung Lee, Yuliya Lierler, Vladimir Lifschitz, Fangkai Yang
Representing First-Order Causal Theories By Logic Programs, Paolo Ferrarris, Joohyung Lee, Yuliya Lierler, Vladimir Lifschitz, Fangkai Yang
Computer Science Faculty Publications
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.
A Tarskian Informal Semantics For Answer Set Programming, Marc Denecker, Yuliya Lierler, Miroslaw Truszczyński, Joost Vennekens
A Tarskian Informal Semantics For Answer Set Programming, Marc Denecker, Yuliya Lierler, Miroslaw Truszczyński, Joost Vennekens
Computer Science Faculty Proceedings & Presentations
In their seminal papers on stable model semantics, Gelfond and Lifschitz introduced ASP by casting programs as epistemic theories, in which rules represent statements about the knowledge of a rational agent. To the best of our knowledge, theirs is still the only published systematic account of the intuitive meaning of rules and programs under the stable semantics. In current ASP practice, however, we find numerous applications in which rational agents no longer seem to play any role. Therefore, we propose here an alternative explanation of the intuitive meaning of ASP programs, in which they are not viewed as statements about …
Weighted-Sequence Problem: Asp Vs Casp And Declarative Vs Problem-Oriented Solving, Yuliya Lierler, Shaden Smith
Weighted-Sequence Problem: Asp Vs Casp And Declarative Vs Problem-Oriented Solving, Yuliya Lierler, Shaden Smith
Computer Science Faculty Proceedings & Presentations
Search problems with large variable domains pose a challenge to current answer-set programming (ASP) systems as large variable domains make grounding take a long time, and lead to large ground theories that may make solving infeasible. To circumvent the “grounding bottleneck” researchers proposed to integrate constraint solving techniques with ASP in an approach called constraint ASP (CASP). In the paper, we evaluate an ASP system clingo and a CASP system clingcon on a handcrafted problem involving large integer domains that is patterned after the database task of determining the optimal join order. We find that search methods used by clingo …
On The Relation Of Constraint Answer Set Programming Languages And Algorithms, Yuliya Lierler
On The Relation Of Constraint Answer Set Programming Languages And Algorithms, Yuliya Lierler
Computer Science Faculty Proceedings & Presentations
Recently a logic programming language AC was proposed by Mellarkod et al. (2008) to integrate answer set programming (ASP) and constraint logic programming. Similarly, Gebser et al. (2009) proposed a CLINGCON language integrating ASP and finite domain constraints. These languages allow new efficient inference algorithms that combine traditional ASP procedures and other methods in constraint programming. In this paper we show that a transition system introduced by Nieuwenhuis et al. (2006) to model SAT solvers can be extended to model the “hybrid” ACSOLVER algorithm by Mellarkod et al. developed for simple AC programs and the CLINGCON algorithm by Gebser et …
Practical And Methodological Aspects Of The Use Of Cutting-Edge Asp Tools, Marcello Balduccini, Yuliya Lierler
Practical And Methodological Aspects Of The Use Of Cutting-Edge Asp Tools, Marcello Balduccini, Yuliya Lierler
Computer Science Faculty Proceedings & Presentations
In the development of practical applications of answer set programming (ASP), encodings that use well-established solvers such as CLASP and DLV are sometimes affected by scalability issues. In those situations, one can resort to more sophisticated ASP tools exploiting, for instance, incremental and constraint ASP. However, today there is no specific methodology for the selection or use of such tools. In this paper we describe how we used such cutting-edge ASP tools on challenging problems from the Third Answer Set Programming Competition. We view this paper as a first step in the development of a general methodology for the use …
Surviving Solver Sensitivity: An Asp Practitioner’S Guide, Bryan Silverthorn, Yuliya Lierler, Marius Schneider
Surviving Solver Sensitivity: An Asp Practitioner’S Guide, Bryan Silverthorn, Yuliya Lierler, Marius Schneider
Computer Science Faculty Proceedings & Presentations
Answer set programming (ASP) is a declarative programming formalism that allows a practitioner to specify a problem without describing an algorithm for solving it. In ASP, the tools for processing problem specifications are called answer set solvers. Because specified problems are often NP complete, these systems often require significant computational effort to succeed. Furthermore, they offer different heuristics, expose numerous parameters, and their running time is sensitive to the configuration used. Portfolio solvers and automatic algorithm configuration systems are recent attempts to automate the problem of manual parameter tuning, and to mitigate the burden of identifying the right solver configuration. …
Abstract Answer Set Solvers With Backjumping And Learning, Yuliya Lierler
Abstract Answer Set Solvers With Backjumping And Learning, Yuliya Lierler
Computer Science Faculty Publications
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.
Termination Of Grounding Is Not Preserved By Strongly Equivalent Transformations, Yuliya Lierler, Vladimir Lifschitz
Termination Of Grounding Is Not Preserved By Strongly Equivalent Transformations, Yuliya Lierler, Vladimir Lifschitz
Computer Science Faculty Proceedings & Presentations
The operation of a typical answer set solver begins with grounding—replacing the given program with a program without variables that has the same answer sets. When the given program contains function symbols, the process of grounding may not terminate. In this note we give an example of a pair of consistent, strongly equivalent programs such that one of them can be grounded by LPARSE, DLV, and gringo, and the other cannot.
Parsing Combinatory Categorial Grammar With Answer Set Programming: Preliminary Report, Yuliya Lierler, Peter Schüller
Parsing Combinatory Categorial Grammar With Answer Set Programming: Preliminary Report, Yuliya Lierler, Peter Schüller
Computer Science Faculty Proceedings & Presentations
Combinatory categorial grammar (CCG) is a grammar formalism used for natural language parsing. CCG assigns structured lexical categories to words and uses a small set of combinatory rules to combine these categories to parse a sentence. In this work we propose and implement a new approach to CCG parsing that relies on a prominent knowledge representation formalism, answer set programming (ASP) — a declarative programming paradigm. We formulate the task of CCG parsing as a planning problem and use an ASP computational tool to compute solutions that correspond to valid parses. Compared to other approaches, there is no need to …
Sat-Based Answer Set Programming, Yuliya Lierler
Sat-Based Answer Set Programming, Yuliya Lierler
Computer Science Faculty Publications
Answer set programming (ASP) is a declarative programming paradigm oriented towards difficult combinatorial search problems. Syntactically, ASP programs look like Prolog programs, but solutions are represented in ASP by sets of atoms, and not by substitutions, as in Prolog. Answer set systems, such as SMODELS, SMODELSCC, and DLV, compute answer sets of a given program in the sense of the answer set (stable model) semantics. This is different from the functionality of Prolog systems, which determine when a given query is true relative to a given logic program. ASP has been applied to many areas of science and technology, from …
One More Decidable Class Of Finitely Ground Programs, Yuliya Lierler, Vladimir Lifschitz
One More Decidable Class Of Finitely Ground Programs, Yuliya Lierler, Vladimir Lifschitz
Computer Science Faculty Proceedings & Presentations
When a logic program is processed by an answer set solver, the first task is to generate its instantiation. In a recent paper, Calimeri et el. made the idea of efficient instantiation precise for the case of disjunctive programs with function symbols, and introduced the class of “finitely ground” programs that can be efficiently instantiated. Since that class is undecidable, it is important to find its large decidable subsets. In this paper, we introduce such a subset—the class of argumentrestricted programs. It includes, in particular, all finite domain programs, ω-restricted programs, and λ-restricted programs.
Model Generation For Generalized Quantifiers Via Answer Set Programming, Yuliya Lierler, Günther Görz
Model Generation For Generalized Quantifiers Via Answer Set Programming, Yuliya Lierler, Günther Görz
Computer Science Faculty Proceedings & Presentations
For the semantic evaluation of natural language sentences, in particular those containing generalized quantifiers, we subscribe to the generate and test methodology to produce models of such sentences. These models are considered as means by which the sentences can be interpreted within a natural language processing system. The goal of this paper is to demonstrate that answer set programming is a simple, efficient and particularly well suited model generation technique for this purpose, leading to a straightforward implementation.
Experiments With Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea, A. Tacchella
Experiments With Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea, A. Tacchella
Computer Science Faculty Proceedings & Presentations
Answer Set Programming (ASP) emerged in the late 1990s as a new logic programming paradigm which has been successfully applied in various application domains. Propositional satisfiability (SAT) is one of the most studied problems in Computer Science. ASP and SAT are closely related: Recent works have studied their relation, and efficient SAT-based ASP solvers (like assat and Cmodels) exist. In this paper we report about (i) the extension of the basic procedures in Cmodels in order to incorporate the most popular SAT reasoning strategies, and (ii) an extensive comparative analysis involving also other state-of-the-art answer set solvers. The experimental analysis …
Disjunctive Answer Set Programming Via Satisfiability, Yuliya Lierler
Disjunctive Answer Set Programming Via Satisfiability, Yuliya Lierler
Computer Science Faculty Proceedings & Presentations
Using SAT solvers as inference engines in answer set programming systems showed to be a promising approach in building efficient systems. Nowadays SAT based answer set programming systems successfully work with nondisjunctive programs. This paper proposes a way to use SAT solvers for finding answer sets for disjunctive logic programs. We implement two different ways of SAT solver invocation used in nondisjunctive answer set programming. The algorithms are based on the definition of completion for disjunctive programs and the extension of loop formula to the disjunctive case. We propose the necessary modifications to the algorithms known for nondisjunctive programs in …
Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Computer Science Faculty Proceedings & Presentations
The relation between answer set programming (ASP) and propositional satisfiability (SAT) is at the center of many research papers, partly because of the tremendous performance boost of SAT solvers during last years. Various translations from ASP to SAT are known but the resulting SAT formula either includes many new variables or may have an unpractical size. There are also well known results showing a one-to-one correspondence between the answer sets of a logic program and the models of its completion. Unfortunately, these results only work for specific classes of problems. In this paper we present a SAT-based decision procedure for …
Computing Answer Sets Of A Logic Program Via-Enumeration Of Sat Certificates, Yuliya Lierler, Marco Maratea
Computing Answer Sets Of A Logic Program Via-Enumeration Of Sat Certificates, Yuliya Lierler, Marco Maratea
Computer Science Faculty Proceedings & Presentations
Answer set programming is a new programming paradigm proposed based on the answer set semantics of Prolog. It is well known that an answer set for a logic program is also a model of the program's completion. The converse is true when the logic program is "tight". Lin and Zhao showed that for non-tight programs the models of completion which do not correspond to answer sets can be eliminated by adding to the completion what they called "loop formulas". Nevertheless, their solver ASSAT 1 has some disadvantages: it can work only with basic rules, and it can compute only one …