Physical Sciences and Mathematics Commons^™

Abstract Modular Inference Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński

Yuliya Lierler

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.

Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea

Yuliya Lierler

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 …

Disjunctive Answer Set Programming Via Satisfiability, Yuliya Lierler

Yuliya Lierler

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 …

Transition Systems For Model Generators — A Unifying Approach, Yuliya Lierler, Miroslaw Truszczyński

Yuliya Lierler

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 answerset 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. …

Logic Programs Vs. First-Order Formulas In Textual Inference, Yuliya Lierler, Vladimir Lifschitz

Yuliya Lierler

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 …

Elementary Sets For Logic Programs, Martin Gebser, Joohyung Lee, Yuliya Lierler

Yuliya Lierler

By introducing the concepts of a loop and a loop formula, Lin and Zhao showed that the answer sets of a nondisjunctive logic program are exactly the models of its Clark’s completion that satisfy the loop formulas of all loops. Recently, Gebser and Schaub showed that the Lin-Zhao theorem remains correct even if we restrict loop formulas to a special class of loops called “elementary loops.” In this paper, we simplify and generalize the notion of an elementary loop, and clarify its role. We propose the notion of an elementary set, which is almost equivalent to the notion of an …

Goal-Converging Behavior Networks And Self-Solving Planning Domains, Bernhard Nebel, Yuliya Lierler

Yuliya Lierler

Agents operating in the real world have to deal with a constantly changing and only partially predictable environment and are nevertheless expected to choose reasonable actions quickly. One way to address this problem is to use behavior networks as proposed by Maes, which support real-time decision making. Robotic soccer appears to be one domain where behavior networks have been proven to be particularly successful. In this paper, we analyze the reason for the success by identifying conditions that make behavior networks goal converging, i.e., allow them to reach the goals regardless of which particular action selection scheme is used. In …

A Tarskian Informal Semantics For Answer Set Programming, Marc Denecker, Yuliya Lierler, Miroslaw Truszczyński, Joost Vennekens

Yuliya Lierler

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 …

Head-Elementary-Set-Free Logic Programs, Martin Gebser, Joohyung Lee, Yuliya Lierler

Yuliya Lierler

The recently proposed notion of an elementary set yielded a refinement of the theorem on loop formulas, telling us that the stable models of a disjunctive logic program can be characterized by the loop formulas of its elementary sets. Based on the notion of an elementary set, we propose the notion of head-elementary-set-free (HEF) programs, a more general class of disjunctive programs than head-cycle-free (HCF) programs proposed by Ben-Eiiyahu and Dechter. that can still be turned into nondisjunct:ive programs in polynomial time and space by "shifting" the head atoms into the body. We show several properties of HEF programs that …

Termination Of Grounding Is Not Preserved By Strongly Equivalent Transformations, Yuliya Lierler, Vladimir Lifschitz

Yuliya Lierler

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.

Towards A Tight Integration Of Syntactic Parsing With Semantic Disambiguation By Means Of Declarative Programming, Yuliya Lierler, Peter Schüller

Yuliya Lierler

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.

One More Decidable Class Of Finitely Ground Programs, Yuliya Lierler, Vladimir Lifschitz

Yuliya Lierler

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.

Automatic Compilation Of Protocol Insecurity Problems Into Logic Programming, Alessandro Armondo, Luca Compagna, Yuliya Lierler

Yuliya Lierler

In this paper we show how protocol insecurity problems expressed in a multi-set rewriting formalism can be automatically translated into logic programming problems. The proposed translation paves the way to the construction of model-checkers for security protocols based on state-of-the-art solvers for logic programs. We have assessed the effectiveness of the approach by running the proposed reduction against a selection of insecurity problems drawn from the Clark & Jacob library of security protocols: by running state-of-the-art solvers against the resulting logic programming problems most of the (known) attacks on the considered protocols are found in a few seconds.

Research Challenges And Opportunities In Knowledge Representation, Section 2.4.2 Advances In Satisfiability And Answer Set Programming, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Yuliya Lierler

Final report edited by Natasha Noy and Deborah McGuinness. Report Section 2.4.2, Advances in satisfiability and answer set programming, authored by Yuliya Lierer, UNO faculty member.

Research Challenges And Opportunities In Knowledge Representation, Section 4.1.1 Hybrid Kr, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Yuliya Lierler

Final report edited by Natasha Noy and Deborah McGuinness. Report Section 4.1.1 Hybrid KR, co-authored by Yuliya Lierer, UNO faculty member.

Parsing Combinatory Categorial Grammar Via Planning In Answer Set Programming, Yuliya Lierler, Peter Schueller

Yuliya Lierler