Vernon Asuncion

JAIR Journal 2019 Journal Article

Polynomial and Exponential Bounded Logic Programs with Function Symbols: Some New Decidable Classes

• Vernon Asuncion
• Yan Zhang
• Heng Zhang
• Ruixuan Li

A logic program with function symbols is called finitely ground if there is a finite propositional logic program whose stable models are exactly the same as the stable models of this program. Finite groundability is an important property for logic programs with function symbols because it makes feasible to compute such programs' stable models using traditional ASP solvers. In this paper, we introduce new decidable classes of finitely ground programs called poly-bounded and k-EXP-bounded programs, which, to the best of our knowledge, strictly contain all other decidable classes of finitely ground programs discovered so far in the literature. We also study the relevant complexity properties for these classes of programs. We prove that the membership complexities for poly-bounded and k-EXP-bounded programs are EXPTIME-complete and (k+1)-EXPTIME-complete, respectively.

KR Conference 2018 Short Paper

Loop Restricted Existential Rules and First-order Rewritability for Query Answering

• Vernon Asuncion
• Yan Zhang
• Heng Zheng

AAAI Conference 2017 Conference Paper

Polynomially Bounded Logic Programs with Function Symbols: A New Decidable

• Vernon Asuncion
• Yan Zhang
• Heng Zhang

A logic program with function symbols is called finitely ground if there is a finite propositional logic program whose stable models are exactly the same as the stable models of this program. Finite groundability is an important property for logic programs with function symbols because it makes feasible to compute such program’s stable models using traditional ASP solvers. In this paper, we introduce a new decidable class of finitely ground programs called POLY-bounded programs, which, to the best of our knowledge, strictly contains all decidable classes of finitely ground programs discovered so far in the literature. We also study the related complexity property for this class of programs. We prove that deciding whether a program is POLY-bounded is EXPTIMEcomplete.

AIJ Journal 2015 Journal Article

Ordered completion for logic programs with aggregates

• Vernon Asuncion
• Yin Chen
• Yan Zhang
• Yi Zhou

We consider the problem of translating first-order answer set programs with aggregates into first-order sentences with the same type of aggregates. In particular, we show that, on finite structures, normal logic programs with convex aggregates, which cover both monotone and antimonotone aggregates as well as the aggregates appearing in most benchmark programs, can always be captured in first-order logic with the same type of aggregates by introducing auxiliary predicates. More precisely, we prove that every finite stable model of a normal program with convex aggregates is corresponding to a classical model of its enhanced ordered completion. This translation then suggests an alternative way for computing the stable models of such kind of programs. We report some experimental results, which demonstrate that our solver GROCv2 is comparable to the state-of-the-art answer set solvers. We further show that convex aggregates form a maximal class for this purpose. That is, we can always construct a normal logic program under any given non-convex aggregate context and prove that it can never be translated into first-order sentences with the same type of aggregates unless NP = coNP.

KR Conference 2014 Conference Paper

Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness

• Vernon Asuncion
• Yan Zhang
• Heng Zhang

Logic programs with ordered disjunction (LPODs) (Brewka 2002) generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including game theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to capture the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally represents the reasoning procedure of LPODs. We show that on finite structures, every LPOD can be translated to a firstorder sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture first-order normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure. A ← not C B ← not D A ← not C C ← not D, not B B ← not C, not A B ← not D B ← not C, not A C ← not D, not B. Then the class of stable models of Π consists of all stable models of these four split programs, which is {{A, B}, {B}, {C}}. Then by integrating proper preference relation among these stable models, the preferred stable models can be obtained for an LPOD. There have been several extensions of LPODs in recent years: Karger et al (2008) extended LPODs by allowing both ordered and unordered disjunction in the heads of rules; Confalonieri et al (2010) recently defined a possibilistic semantics for LPODs in order to handle uncertainty; and Cabalar (2011) also proposed a direct translation from LPODs to normal logic programs via the logic of Here-and-There. It has been argued that LPODs provide a natural way to deal with preference in reasoning that are useful in various applications such as game theory, policy languages, planning and argumentations (Brewka 2002; Cabalar 2011; Confalonieri et al. 2010). On the other hand, in recent years, Answer Set Programming (ASP) has been generalized to arbitrary first-order sentences (Ferraris, Lee, and Lifschitz 2011). One challenging research along this direction is to establish proper logical and computational foundations for promoting useful functionalities in existing ASP paradigm to the first-order level. A number of topics in this aspect have been investigated and relevant properties revealed, e. g., (Asuncion et al. 2012; Asuncion, Zhang, and Zhou 2013; Lee and Meng 2011; Babb and Lee 2012). One major advantage of first-order ASP is that it provides a succinct declarative language, in which the underlying problem constraints (rules) may be completely separated from concrete problem instances, and hence more flexible for problem representation and modeling (Lin and Zhou 2011). In this paper, we study the semantics and expressiveness of LPODs on the first-order level. We make the following main contributions towards this topic: 1. Following the style of general stable model semantics

AIJ Journal 2012 Journal Article

Ordered completion for first-order logic programs on finite structures

• Vernon Asuncion
• Fangzhen Lin
• Yan Zhang
• Yi Zhou

In this paper, we propose a translation from normal first-order logic programs under the stable model semantics to first-order sentences on finite structures. The translation is done through, what we call, ordered completion which is a modification of Clarkʼs completion with some auxiliary predicates added to keep track of the derivation order. We show that, on finite structures, classical models of the ordered completion of a normal logic program correspond exactly to the stable models of the program. We also extend this result to normal programs with constraints and choice rules. From a theoretical viewpoint, this work clarifies the relationships between normal logic programming under the stable model semantics and classical first-order logic. It follows that, on finite structures, every normal program can be defined by a first-order sentence if new predicates are allowed. This is a tight result as not every normal logic program can be defined by a first-order sentence if no extra predicates are allowed or when infinite structures are considered. Furthermore, we show that the result cannot be extended to disjunctive logic programs, assuming that NP ≠ coNP. From a practical viewpoint, this work leads to a new type of ASP solver by grounding on a programʼs ordered completion instead of the program itself. We report on a first implementation of such a solver based on several optimization techniques. Our experimental results show that our solver compares favorably to other major ASP solvers on the Hamiltonian Circuit program, especially on large domains.

AAAI Conference 2012 Conference Paper

Ordered Completion for Logic Programs with Aggregates

• Vernon Asuncion
• Yan Zhang
• Yi Zhou

In this paper, we show that first-order logic programs with monotone aggregates under the stable model semantics can be captured in classical first-order logic. More precisely, we extend the notion of ordered completion for logic programs with a large variety of aggregates so that every stable model of a program with aggregates corresponds to a classical model of its enhanced ordered completion, and vice versa.

AAAI Conference 2010 Conference Paper

Ordered Completion for First-Order Logic Programs on Finite Structures

• Vernon Asuncion
• Fangzhen Lin
• Yan Zhang
• Yi Zhou

In this paper, we propose a translation from normal first-order logic programs under the answer set semantics to first-order theories on finite structures. Specifically, we introduce ordered completions which are modifications of Clark’s completions with some extra predicates added to keep track of the derivation order, and show that on finite structures, classical models of the ordered-completion of a normal logic program correspond exactly to the answer sets (stable models) of the logic program.