System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers

• URL: http://arxiv.org/abs/2506.10708v1
• Date: Thu, 12 Jun 2025 13:59:15 GMT
• Title: System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
• Abstract summary: 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.
• Score: 3.677571687801579
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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 ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable models of ASPMT programs. In this paper we present a compiler called {\sc aspsmt2smt}, which implements this translation. The system uses ASP grounder {\sc gringo} and SMT solver {\sc z3}. {\sc gringo} partially grounds input programs while leaving some variables to be processed by {\sc z3}. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.

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)
• $\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)
• 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)
• Self-Steering Language Models [113.96916935955842]
  DisCIPL is a method for "self-steering" language models (LMs)<n>DisCIPL generates a task-specific inference program that is executed by a population of Follower models.<n>Our work opens up a design space of highly-parallelized Monte Carlo inference strategies.
  arXiv  Detail & Related papers  (2025-04-09T17:54:22Z)
• (How) Do Language Models Track State? [50.516691979518164]
  Transformer language models (LMs) exhibit behaviors that appear to require tracking the unobserved state of an evolving world.<n>We study state tracking in LMs trained or fine-tuned to compose permutations.<n>We show that LMs consistently learn one of two state tracking mechanisms for this task.
  arXiv  Detail & Related papers  (2025-03-04T18:31:02Z)
• Towards Zero-Shot Multimodal Machine Translation [64.9141931372384]
  We propose a method to bypass the need for fully supervised data to train multimodal machine translation systems.<n>Our method, called ZeroMMT, consists in adapting a strong text-only machine translation (MT) model by training it on a mixture of two objectives.<n>To prove that our method generalizes to languages with no fully supervised training data available, we extend the CoMMuTE evaluation dataset to three new languages: Arabic, Russian and Chinese.
  arXiv  Detail & Related papers  (2024-07-18T15:20:31Z)
• Self-Modifying State Modeling for Simultaneous Machine Translation [25.11963998838586]
  Simultaneous Machine Translation (SiMT) generates target outputs while receiving stream source inputs. Existing SiMT methods, which learn the policy by exploring various decision paths in training, face inherent limitations. We propose textbfSelf-textbfModifying textbfState textbfModeling (SM$2$), a novel training paradigm for SiMT task.
  arXiv  Detail & Related papers  (2024-06-04T11:57:58Z)
• Cross-Modal Multi-Tasking for Speech-to-Text Translation via Hard Parameter Sharing [72.56219471145232]
  We propose a ST/MT multi-tasking framework with hard parameter sharing. Our method reduces the speech-text modality gap via a pre-processing stage. We show that our framework improves attentional encoder-decoder, Connectionist Temporal Classification (CTC), transducer, and joint CTC/attention models by an average of +0.5 BLEU.
  arXiv  Detail & Related papers  (2023-09-27T17:48:14Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42: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)
• Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks [108.4568236569645]
  Chain-of-thoughts prompting (CoT) is by far the state-of-art method for these tasks. We propose Program of Thoughts' (PoT), which uses language models to express the reasoning process as a program. PoT can show an average performance gain over CoT by around 12% across all the evaluated datasets.
  arXiv  Detail & Related papers  (2022-11-22T21:06:00Z)
• Modeling Dual Read/Write Paths for Simultaneous Machine Translation [21.03142288187605]
  We propose a method of Dual Path SiMT which introduces duality constraints to guide the read/write path. Experiments on En-Vi and De-En SiMT tasks show that our method can outperform strong baselines under all latency.
  arXiv  Detail & Related papers  (2022-03-17T08:35:36Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) and Transformers are two popular neural architectures used for natural language processing tasks. In practice, it is often observed that Transformer models have better representation power than LSTM. We study such practical differences between LSTM and Transformer and propose an explanation based on their latent space decomposition patterns.
  arXiv  Detail & Related papers  (2021-12-16T19:56:44Z)

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.