Answer Set Programming Modulo Theories and Reasoning about Continuous Changes
- URL: http://arxiv.org/abs/2507.04299v1
- Date: Sun, 06 Jul 2025 08:52:03 GMT
- Title: Answer Set Programming Modulo Theories and Reasoning about Continuous Changes
- Abstract summary: ASPMT is a new framework of tight integration of answer set programming (ASP) and satisfiability modulo theories (SMT)<n>We demonstrate the usefulness of ASPMT by enhancing action language C+ to handle continuous changes as well as discrete changes.
- Score: 3.677571687801579
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
Related papers
- EZSMT Version 3, Matured [2.4387391584956]
This paper presents the design and implementation of EZSMTV3, an SMT-based CASP framework that advances the translational approach to CASP solving.<n>Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types.<n>The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP]
arXiv Detail & Related papers (2026-07-15T00:07:15Z) - In-Context Model Predictive Generation: Open-Vocabulary Motion Synthesis from Language Models to Physics [109.99871326497333]
In-Context Model Predictive Generation (ICMPG) is a framework that integrates language-model planning with inference-time physical feedback.<n>ICMPG reformulates motion synthesis as a Model Predictive Control (MPC)-like process with two modules.
arXiv Detail & Related papers (2026-06-25T12:50:33Z) - Functional Stable Model Semantics and Answer Set Programming Modulo Theories [2.294331241389926]
Intensional functions are those whose values can be described by other functions and predicates.<n>We show that functional stable model semantics plays an important role in the framework of ASPMT.
arXiv Detail & Related papers (2026-05-10T13:19:32Z) - $\mathcal{S}^2$IT: Stepwise Syntax Integration Tuning for Large Language Models in Aspect Sentiment Quad Prediction [51.165432266846096]
syntactic structure information is underutilized in the generative paradigm of large language models (LLMs)<n>S2IT progressively integrates syntactic structure knowledge into LLMs through a multi-step tuning process.<n> Experiments demonstrate that S2IT significantly improves state-of-the-art performance across multiple datasets.
arXiv Detail & Related papers (2026-04-25T13:24:29Z) - The Meta-Prompting Protocol: Orchestrating LLMs via Adversarial Feedback Loops [0.6345523830122167]
Meta-Prompt Protocol formalizes the orchestration of Large Language Models as a programmable, self-optimizing system.<n>Treating natural language instructions as differentiable variables within a semantic graph and utilizing textual critiques as gradients, this architecture mitigates hallucination and prevents model collapse.
arXiv Detail & Related papers (2025-12-17T03:32:21Z) - System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers [3.677571687801579]
ASPMT is an approach to combining answer set programming and satisfiability modulo theories.<n>It is shown that the tight fragment of ASPMT programs can be turned into SMT instances.<n>We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.
arXiv Detail & Related papers (2025-06-12T13:59:15Z) - The Unreasonable Effectiveness of Model Merging for Cross-Lingual Transfer in LLMs [54.59207567677249]
Large language models (LLMs) still struggle across tasks outside of high-resource languages.<n>In this work, we investigate cross-lingual transfer to lower-resource languages where task-specific post-training data is scarce.
arXiv Detail & Related papers (2025-05-23T20:28:31Z) - Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo [90.78001821963008]
A wide range of LM applications require generating text that conforms to syntactic or semantic constraints.<n>We develop an architecture for controlled LM generation based on sequential Monte Carlo (SMC)<n>Our system builds on the framework of Lew et al. (2023) and integrates with its language model probabilistic programming language.
arXiv Detail & Related papers (2025-04-17T17:49:40Z) - Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps.<n>We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths.<n>SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
arXiv Detail & Related papers (2025-04-13T13:35:41Z) - Training of Scaffolded Language Models with Language Supervision: A Survey [62.59629932720519]
This survey organizes the literature on the design and optimization of emerging structures around post-trained LMs.<n>We refer to this overarching structure as scaffolded LMs and focus on LMs that are integrated into multi-step processes with tools.
arXiv Detail & Related papers (2024-10-21T18:06:25Z) - LangSuitE: Planning, Controlling and Interacting with Large Language Models in Embodied Text Environments [70.91258869156353]
We introduce LangSuitE, a versatile and simulation-free testbed featuring 6 representative embodied tasks in textual embodied worlds.
Compared with previous LLM-based testbeds, LangSuitE offers adaptability to diverse environments without multiple simulation engines.
We devise a novel chain-of-thought (CoT) schema, EmMem, which summarizes embodied states w.r.t. history information.
arXiv Detail & Related papers (2024-06-24T03:36:29Z) - An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes [4.393684402895834]
Algebraic data types (ADTs) are a construct classically found in functional programming languages.
We present an SMT solver that takes a fundamentally different approach, an empheager approach.
arXiv Detail & Related papers (2023-10-18T18:14:18Z) - First-Order Stable Model Semantics with Intensional Functions [2.1955512452222696]
We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions.
We use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT)
ASPMT can be applied to domains containing real numbers and alleviates the grounding problem.
arXiv Detail & Related papers (2023-07-15T06:03:35Z) - On Conditional and Compositional Language Model Differentiable Prompting [75.76546041094436]
Prompts have been shown to be an effective method to adapt a frozen Pretrained Language Model (PLM) to perform well on downstream tasks.
We propose a new model, Prompt Production System (PRopS), which learns to transform task instructions or input metadata, into continuous prompts.
arXiv Detail & Related papers (2023-07-04T02:47:42Z) - Explicitly Modeling Syntax in Language Models with Incremental Parsing
and a Dynamic Oracle [88.65264818967489]
We propose a new syntax-aware language model: Syntactic Ordered Memory (SOM)
The model explicitly models the structure with an incremental and maintains the conditional probability setting of a standard language model.
Experiments show that SOM can achieve strong results in language modeling, incremental parsing and syntactic generalization tests.
arXiv Detail & Related papers (2020-10-21T17:39:15Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.