First-Order Stable Model Semantics with Intensional Functions

• URL: http://arxiv.org/abs/2307.10225v1
• Date: Sat, 15 Jul 2023 06:03:35 GMT
• Title: First-Order Stable Model Semantics with Intensional Functions
• Abstract summary: 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.
• Score: 2.1955512452222696
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 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.

Related papers

• From Fixed Keys to Readable Schemas: Small Language Models for Vehicle Agent Function Calls [9.651124018371158]
  In-vehicle assistants must translate natural-language requests into accurate vehicle function calls under strict memory and latency constraints.<n>Two approaches are to represent each function with a dedicated Functional Token (FT) or provide function schemas directly in the prompt.<n>FTs enable compact inference but are restricted to functions learned during training, whereas SIP can generalize to unseen functions at the cost of longer prompts.
  arXiv  Detail & Related papers  (2026-09-08T21:46:35Z)
• Domain-Specific Data Synthesis for LLMs via Minimal Sufficient Representation Learning [72.60775633696593]
  Large Language Models can achieve strong performance in specific domains through fine-tuning on domain-specific data.<n>Existing data synthesis approaches rely on explicit domain descriptions expressed in natural language and careful prompt engineering.<n>We propose a novel framework, DOMINO, that learns a minimal sufficient domain representation from reference samples and leverages it to guide the generation of domain-aligned synthetic data.
  arXiv  Detail & Related papers  (2026-05-28T14:57:02Z)
• Formal Verification of Imperative First-Class Functions in Move [2.6265820258267794]
  Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language.<n>This paper describes the representation of function values in the Move specification language and their implementation in MVP.
  arXiv  Detail & Related papers  (2026-05-11T05:31:55Z)
• 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)
• Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications [2.5164739639003364]
  We extend mining procedures to operate over richer datatypes.<n>We demonstrate our approach reactive programs from mined specifications on the OpenAI-Gymnasium ToyText environments.
  arXiv  Detail & Related papers  (2026-03-05T19:56:25Z)
• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• SemaMIL: Semantic-Aware Multiple Instance Learning with Retrieval-Guided State Space Modeling for Whole Slide Images [17.674866281320046]
  SemaMIL is an adaptive method for extracting discriminative features from whole slide images.<n>It clusters semantically similar patches in sequence through a reversible permutation.<n>It achieves state-of-the-art subtype accuracy with fewer FLOPs and parameters.
  arXiv  Detail & Related papers  (2025-08-30T10:13: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)
• Graft: Integrating the Domain Knowledge via Efficient Parameter Synergy for MLLMs [56.76586846269894]
  Multimodal Large Language Models (MLLMs) have achieved success across various domains.<n>Despite its importance, the study of knowledge sharing among domain-specific MLLMs remains largely underexplored.<n>We propose a unified parameter integration framework that enables modular composition of expert capabilities.
  arXiv  Detail & Related papers  (2025-06-30T15:07:41Z)
• $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$ is a unified approach that enforces rich context-sensitive constraints and task- and instance-specific semantics directly on an LLM decoder. texttSEM-CTRL$ allows small pre-trained LLMs to efficiently outperform larger variants and state-of-the-art reasoning models.
  arXiv  Detail & Related papers  (2025-03-03T18:33:46Z)
• Simultaneous and Meshfree Topology Optimization with Physics-informed Gaussian Processes [0.0]
  Topology optimization (TO) provides a principled mathematical approach for optimizing the performance of a structure by designing its material spatial distribution in a pre-defined domain and subject to a set of constraints. We develop a new class of TO methods based on the framework of Gaussian processes (GPs) whose mean functions are parameterized via deep neural networks. To test our method against conventional TO approaches implemented in commercial software, we evaluate it on four problems involving the minimization of dissipated power in Stokes flow.
  arXiv  Detail & Related papers  (2024-08-07T01:01:35Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  This paper introduces TLINet, a neural-symbolic framework for learning STL formulas. In contrast to existing approaches, we introduce approximation methods for max operator designed specifically for temporal logic-based gradient techniques. Our framework not only learns the structure but also the parameters of STL formulas, allowing flexible combinations of operators and various logical structures.
  arXiv  Detail & Related papers  (2024-05-03T16:38:14Z)
• AMOR: A Recipe for Building Adaptable Modular Knowledge Agents Through Process Feedback [91.76169903959376]
  We present AMOR, an agent framework based on open-source large language models (LLMs) AMOR builds reasoning logic over a finite state machine (FSM) that solves problems through autonomous executions and transitions over disentangled modules. Based on this reasoning and feedback framework, we develop AMOR through two-stage fine-tuning: warm-up and adaptation.
  arXiv  Detail & Related papers  (2024-02-02T14:56:48Z)
• Composing Parameter-Efficient Modules with Arithmetic Operations [20.119291936493788]
  We propose to compose parameter-efficient modules through linear arithmetic operations in the weight space. Our approach requires emphno additional training and enables highly flexible module composition. We extend our approach to detoxify Alpaca-LoRA, the latest instruction-tuned large language model based on LLaMA.
  arXiv  Detail & Related papers  (2023-06-26T17:33:21Z)
• $\omega$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs [64.25762042361839]
  $omega$PAP spaces are spaces for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs. We establish the almost-everywhere differentiability of probabilistic programs' trace density functions.
  arXiv  Detail & Related papers  (2023-02-21T12:50:05Z)
• Neural Estimation of Submodular Functions with Applications to Differentiable Subset Selection [50.14730810124592]
  Submodular functions and variants, through their ability to characterize diversity and coverage, have emerged as a key tool for data selection and summarization. We propose FLEXSUBNET, a family of flexible neural models for both monotone and non-monotone submodular functions.
  arXiv  Detail & Related papers  (2022-10-20T06:00:45Z)
• Guiding the PLMs with Semantic Anchors as Intermediate Supervision: Towards Interpretable Semantic Parsing [57.11806632758607]
  We propose to incorporate the current pretrained language models with a hierarchical decoder network. By taking the first-principle structures as the semantic anchors, we propose two novel intermediate supervision tasks. We conduct intensive experiments on several semantic parsing benchmarks and demonstrate that our approach can consistently outperform the baselines.
  arXiv  Detail & Related papers  (2022-10-04T07:27:29Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Sparsification of Decomposable Submodular Functions [27.070004659301162]
  Submodular functions are at the core of many machine learning and data mining tasks. The number of underlying submodular functions in the original function is so large that we need large amount of time to process it and/or it does not even fit in the main memory. We introduce the notion of sparsification for decomposable submodular functions whose objective is to obtain an accurate approximation of the original function is a (weighted) sum of only a few submodular functions.
  arXiv  Detail & Related papers  (2022-01-18T20:05:25Z)
• Temporal Answer Set Programming [3.263632801414296]
  We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax. In a second part, we focus on practical aspects, defining a syntactic fragment called temporal logic programs closer to ASP, and explain how this has been exploited in the construction of the solver TELINGO.
  arXiv  Detail & Related papers  (2020-09-14T16:13:36Z)
• 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.