arXiv subjects

Joohyung Lee

Publications and source records attributed to Joohyung Lee.

60 records · Page 4Linked to original sources

arXiv2014

First-Order Stable Model Semantics and First-Order Loop Formulas

Lin and Zhaos theorem on loop formulas states that in the propositional case the stable model semantics of a logic program can be completely characterized by propositional loop formulas, but this result does not fully carry over to the first-order case. We investigate the precise relationship between the first-order stable model semantics and first-order loop formulas, and study conditions under which the former can be represented by the latter. In order to facilitate the comparison, we extend the definition of a first-order loop formula which was limited to a nondisjunctive program, to a disjunctive program and to an arbitrary first-order theory. Based on the studied relationship we extend the syntax of a logic program with explicit quantifiers, which allows us to do reasoning involving non-Herbrand stable models using first-order reasoners. Such programs can be viewed as a special class of first-order theories under the stable model semantics, which yields more succinct loop formulas than the general language due to their restricted syntax.

cs.LO↗

arXiv2013

A Functional View of Strong Negation in Answer Set Programming

The distinction between strong negation and default negation has been useful in answer set programming. We present an alternative account of strong negation, which lets us view strong negation in terms of the functional stable model semantics by Bartholomew and Lee. More specifically, we show that, under complete interpretations, minimizing both positive and negative literals in the traditional answer set semantics is essentially the same as ensuring the uniqueness of Boolean function values under the functional stable model semantics. The same account lets us view Lifschitz's two-valued logic programs as a special case of the functional stable model semantics. In addition, we show how non-Boolean intensional functions can be eliminated in favor of Boolean intensional functions, and furthermore can be represented using strong negation, which provides a way to compute the functional stable model semantics using existing ASP solvers. We also note that similar results hold with the functional stable model semantics by Cabalar.

cs.AI↗

arXiv2013

Two New Definitions of Stable Models of Logic Programs with Generalized Quantifiers

We present alternative definitions of the first-order stable model semantics and its extension to incorporate generalized quantifiers by referring to the familiar notion of a reduct instead of referring to the SM operator in the original definitions. Also, we extend the FLP stable model semantics to allow generalized quantifiers by referring to an operator that is similar to the $\sm$ operator. For a reasonable syntactic class of logic programs, we show that the two stable model semantics of generalized quantifiers are interchangeable.

cs.LO↗

arXiv2012

Module Theorem for The General Theory of Stable Models

The module theorem by Janhunen et al. demonstrates how to provide a modular structure in answer set programming, where each module has a well-defined input/output interface which can be used to establish the compositionality of answer sets. The theorem is useful in the analysis of answer set programs, and is a basis of incremental grounding and reactive answer set programming. We extend the module theorem to the general theory of stable models by Ferraris et al. The generalization applies to non-ground logic programs allowing useful constructs in answer set programming, such as choice rules, the count aggregate, and nested expressions. Our extension is based on relating the module theorem to the symmetric splitting theorem by Ferraris et al. Based on this result, we reformulate and extend the theory of incremental answer set computation to a more general class of programs.

cs.AI↗

arXiv2011

Representing First-Order Causal Theories by Logic Programs

Nonmonotonic causal logic, introduced by Norman McCain and Hudson Turner, became a 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 first-order causal logic.

cs.AI↗

arXiv2011

On Elementary Loops of Logic Programs

Using the notion of an elementary loop, Gebser and Schaub refined the theorem on loop formulas due to Lin and Zhao by considering loop formulas of elementary loops only. In this article, we reformulate their 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 show that the corresponding problem is {\sf 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 due to Ben-Eliyahu and Dechter. 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.

cs.AI↗