Answer Set Programming Modulo Theories and Reasoning about Continuous Changes
Answer Set Programming Modulo Theories (ASPMT) is a new framework of tight integration of answer set programming (ASP) and satisfiability modulo theories (SMT). Similar to the relationship between first-order logic and SMT, it is based on a recent proposal of the functional stable model semantics by fixing interpretations of background theories. Analogously to a known relationship between ASP and SAT, ``tight'' ASPMT programs can be translated into SMT instances. We demonstrate the usefulness of ASPMT by enhancing action language C+ to handle continuous changes as well as discrete changes. We reformulate the semantics of C+ in terms ofASPMT, and show that SMT solvers can be used to compute the language. We also show how the language can represent cumulative effects on continuous resources.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
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 …
Non-Monotonic Spatial Reasoning with Answer Set Programming Modulo Theories
The systematic modelling of dynamic spatial systems is a key requirement in a wide range of application areas such as commonsense cognitive robotics, computer-aided architecture design, and dynamic geographic information…
Spatial ReasoningASPMT(QS): Non-Monotonic Spatial Reasoning with Answer Set Programming Modulo Theories
The systematic modelling of \emph{dynamic spatial systems} [9] is a key requirement in a wide range of application areas such as comonsense cognitive robotics, computer-aided architecture design, dynamic geographic infor…
Spatial ReasoningFunctional Stable Model Semantics and Answer Set Programming Modulo Theories
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…
Representing Hybrid Automata by Action Language Modulo Theories
Both hybrid automata and action languages are formalisms for describing the evolution of dynamic systems. This paper establishes a formal relationship between them. We show how to succinctly represent hybrid automata in …
Translation