Michael Bartholomew

AIJ Journal 2019 Journal Article

First-order stable model semantics with intensional functions

• Michael Bartholomew
• Joohyung Lee

In classical logic, nonBoolean fluents, such as the location of an object, can be naturally described by functions. However, this is not the case in answer set programs, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions—functions that are specified by a logic program just like predicates are specified. We show that many known properties of the stable model semantics are naturally extended to this formalism and compare it with other related approaches to incorporating intensional functions. Furthermore, we use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT), analogous to the way that Satisfiability Modulo Theories (SMT) is defined, allowing for SMT-like effective first-order reasoning in the context of Answer Set Programming (ASP). Using SMT solving techniques involving functions, ASPMT can be applied to domains containing real numbers and alleviates the grounding problem. We show that other approaches to integrating ASP and CSP/SMT can be related to special cases of ASPMT in which functions are limited to non-intensional ones.

KR Conference 2014 Short Paper

Functional Stable Model Semantics and General Theory of Stable Models

• Michael Bartholomew
• Joohyung Lee

JELIA Conference 2014 Conference Paper

System aspmt2smt: Computing ASPMT Theories by SMT Solvers

• Michael Bartholomew
• Joohyung Lee 0002

Abstract Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable models of ASPMT programs. In this paper we present a compiler called aspsmt2smt, which implements this translation. The system uses ASP grounder gringo and SMT solver z3. gringo partially grounds input programs while leaving some variables to be processed by z3. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.

IJCAI Conference 2013 Conference Paper

Functional Stable Model Semantics and Answer Set Programming Modulo Theories

• Michael Bartholomew
• Joohyung Lee

Recently there has been an increasing interest in incorporating “intensional” functions in answer set programming. Intensional functions are those whose values can be described by other functions and predicates, rather than being pre-defined as in the standard answer set programming. We demonstrate that the functional stable model semantics plays an important role in the framework of “Answer Set Programming Modulo Theories (ASPMT)” —a tight integration of answer set programming and satisfiability modulo theories, under which existing integration approaches can be viewed as special cases where the role of functions is limited. We show that “tight” ASPMT programs can be translated into SMT instances, which is similar to the known relationship between ASP and SAT.

KR Conference 2012 Conference Paper

Stable Models of Formulas with Intensional Functions

• Michael Bartholomew
• Joohyung Lee

In classical logic, nonBoolean fluents, such as the location of an object and the color of a ball, can be naturally described by functions, but this is not the case with the traditional stable model semantics, where the values of functions are predefined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee and Lifschitz to allow intensional functions. The new formalism is closely related to multivalued nonmonotonic causal logic, logic programs with intensional functions, and other extensions of logic programs with functions, while keeping similar properties as those of the first-order stable model semantics. We show how to eliminate intensional functions in favor of intensional predicates and vice versa, and use these results to encode fragments of the language in the input language of ASP solvers and CSP solvers.

IJCAI Conference 2011 Conference Paper

First-Order Extension of the FLP Stable Model Semantics via Modified Circumscription

• Michael Bartholomew
• Joohyung Lee
• Yunsong Meng

We provide reformulations and generalizations of both the semantics of logic programs by Faber, Leone and Pfeifer and its extension to arbitrary propositional formulas by Truszczynski. Unlike the previous definitions, our generalizations refer neither to grounding nor to fixpoints, and apply to first-order formulas containing aggregate expressions. In the same spirit as the first-order stable model semantics proposed by Ferraris, Lee and Lifschitz, the semantics proposed here are based on syntactic transformations that are similar to circumscription. The reformulations provide useful insights into the FLP semantics and its relationship to circumscription and the first-order stable model semantics.

KR Conference 2010 Conference Paper

A Decidable Class of Groundable Formulas in the General Theory of Stable Models

• Michael Bartholomew
• Joohyung Lee

We present a decidable class of first-order formulas in the general theory of stable models that can be instantiated even in the presence of function constants. The notion of an argument-restricted formula presented here is a natural generalization of both the notion of an argument-restricted program and the notion of a semi-safe sentence that have been studied in different contexts. Based on this new notion, we extend the notion of safety defined by Cabalar, Pearce and Valverde to arbitrary formulas that allow function constants, and apply the result to RASPL-1 programs and programs with arbitrary aggregates, ensuring finite groundability of those programs in the presence of function constants. We also show that under a certain syntactic condition, argument-restricted formulas can be turned into argument-restricted programs.