First-order stable model semantics with intensional functions

Michael Bartholomew, Joohyung Lee

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
Pages (from-to)56-93
Number of pages38
JournalArtificial Intelligence
Volume273
DOIs
StatePublished - Aug 1 2019

Fingerprint

Programming theory
Semantics
semantics
programming
Electric grounding
logic
Intensional
Programming
Satisfiability
Values

Keywords

  • Answer set programming
  • Intensional functions
  • Satisfiability modulo theories

ASJC Scopus subject areas

  • Language and Linguistics
  • Linguistics and Language
  • Artificial Intelligence

Cite this

First-order stable model semantics with intensional functions. / Bartholomew, Michael; Lee, Joohyung.

In: Artificial Intelligence, Vol. 273, 01.08.2019, p. 56-93.

Research output: Contribution to journalArticle

@article{de6045e439264167a727cac3519f2476,
title = "First-order stable model semantics with intensional functions",
abstract = "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.",
keywords = "Answer set programming, Intensional functions, Satisfiability modulo theories",
author = "Michael Bartholomew and Joohyung Lee",
year = "2019",
month = "8",
day = "1",
doi = "10.1016/j.artint.2019.01.001",
language = "English (US)",
volume = "273",
pages = "56--93",
journal = "Artificial Intelligence",
issn = "0004-3702",
publisher = "Elsevier",

}

TY - JOUR

T1 - First-order stable model semantics with intensional functions

AU - Bartholomew, Michael

AU - Lee, Joohyung

PY - 2019/8/1

Y1 - 2019/8/1

N2 - 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.

AB - 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.

KW - Answer set programming

KW - Intensional functions

KW - Satisfiability modulo theories

UR - http://www.scopus.com/inward/record.url?scp=85062148233&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85062148233&partnerID=8YFLogxK

U2 - 10.1016/j.artint.2019.01.001

DO - 10.1016/j.artint.2019.01.001

M3 - Article

VL - 273

SP - 56

EP - 93

JO - Artificial Intelligence

JF - Artificial Intelligence

SN - 0004-3702

ER -