Functional Stable Model Semantics and Answer Set Programming Modulo Theories

• URL: http://arxiv.org/abs/2605.09524v1
• Date: Sun, 10 May 2026 13:19:32 GMT
• Title: Functional Stable Model Semantics and Answer Set Programming Modulo Theories
• Abstract summary: 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.
• Score: 2.294331241389926
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• An Operator-Based Approach to STL [10.103844123344057]
  We propose a novel approach to Signal Temporal Logic (STL) based on an operator acting on reachability value functions.<n>This constitutes a new theoretical framework for handling complex multi-nested formulae.<n>In contrast to focusing on the design of STL-based reachability functions, we develop operator-based nesting rules.
  arXiv  Detail & Related papers  (2026-05-27T07:47:45Z)
• Parametric Modular Answer Set Programs Made Declarative [11.52099227565185]
  We introduce a new formalism called parametric modular logic programs, which allows defining subprograms with parameters and intensionality statements.<n>We demonstrate how this formalism can capture the semantics of clingo-programs with collective control, a feature that enables structuring and instantiating subprograms.
  arXiv  Detail & Related papers  (2026-05-21T16:52:18Z)
• Answer Set Programming Modulo Theories and Reasoning about Continuous Changes [3.677571687801579]
  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.
  arXiv  Detail & Related papers  (2025-07-06T08:52:03Z)
• Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries [19.23701821549906]
  We propose a novel framework that combines symbolic execution, large language models (LLMs), and formal verification to generate Relatively Strongest Postconditions (RSPs)<n>Our approach leverages VST-A's symbolic execution to precisely track program execution paths and state transitions.<n>From generated RSPs, we automatically synthesize strongest non-redundant postconditions expressed within given domain specific language.
  arXiv  Detail & Related papers  (2025-06-11T09:33:02Z)
• De-fine: Decomposing and Refining Visual Programs with Auto-Feedback [75.62712247421146]
  De-fine is a training-free framework that decomposes complex tasks into simpler subtasks and refines programs through auto-feedback. Our experiments across various visual tasks show that De-fine creates more robust programs.
  arXiv  Detail & Related papers  (2023-11-21T06:24:09Z)
• 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)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• Text Modular Networks: Learning to Decompose Tasks in the Language of Existing Models [61.480085460269514]
  We propose a framework for building interpretable systems that learn to solve complex tasks by decomposing them into simpler ones solvable by existing models. We use this framework to build ModularQA, a system that can answer multi-hop reasoning questions by decomposing them into sub-questions answerable by a neural factoid single-span QA model and a symbolic calculator.
  arXiv  Detail & Related papers  (2020-09-01T23:45:42Z)
• From Sets to Multisets: Provable Variational Inference for Probabilistic Integer Submodular Models [82.95892656532696]
  Submodular functions have been studied extensively in machine learning and data mining. In this work, we propose a continuous DR-submodular extension for integer submodular functions. We formulate a new probabilistic model which is defined through integer submodular functions.
  arXiv  Detail & Related papers  (2020-06-01T22:20:45Z)

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.