On Loop Formulas with Variables

• URL: http://arxiv.org/abs/2307.10226v1
• Date: Sat, 15 Jul 2023 06:20:43 GMT
• Title: On Loop Formulas with Variables
• Abstract summary: Recently Ferraris, Lee and Lifschitz proposed a new definition of stable models that does not refer to grounding. We show its relation to the idea of loop formulas with variables by Chen, Lin, Wang and Zhang. We extend the syntax of logic programs to allow explicit quantifiers, and define its semantics as a subclass of the new language of stable models.
• Score: 2.1955512452222696
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recently Ferraris, Lee and Lifschitz proposed a new definition of stable models that does not refer to grounding, which applies to the syntax of arbitrary first-order sentences. We show its relation to the idea of loop formulas with variables by Chen, Lin, Wang and Zhang, and generalize their loop formulas to disjunctive programs and to arbitrary first-order sentences. We also extend the syntax of logic programs to allow explicit quantifiers, and define its semantics as a subclass of the new language of stable models by Ferraris et al. Such programs inherit from the general language the ability to handle nonmonotonic reasoning under the stable model semantics even in the absence of the unique name and the domain closure assumptions, while yielding more succinct loop formulas than the general language due to the restricted syntax. We also show certain syntactic conditions under which query answering for an extended program can be reduced to entailment checking in first-order logic, providing a way to apply first-order theorem provers to reasoning about non-Herbrand stable models.

Related papers

• Variational Learning for Insertion-based Generation [50.15012125719375]
  We introduce a probabilistic framework for learning insertion order in variable-length insertion models.<n>We propose the Insertion Process (IP), a generative model that jointly learns where to insert, what to insert, and when to terminate.
  arXiv  Detail & Related papers  (2026-06-01T11:59:46Z)
• An Algebraic View of the Expressivity of Recurrent Language Models [50.88598486616582]
  The paper develops a unified algebraic account of the expressivity of recurrent neural networks.<n>The same architecture cannot implement an even-modulus counter once floating-point recurrences are enforced, yet realizes every even-modulus counter under unsigned-integer quantization.
  arXiv  Detail & Related papers  (2026-06-01T06:47:58Z)
• Generative Recursive Reasoning [67.22973831501257]
  Generative Recursive reAsoning Models (GRAM) is a framework that turns latent reasoning into probabilistic multi-trajectory.<n>GRAM supports conditional reasoning via $p_(y mid x)$ and, with fixed or absent inputs, unconditional generation via $p_(x)$.
  arXiv  Detail & Related papers  (2026-05-19T05:20:56Z)
• Power Term Polynomial Algebra for Boolean Logic [10.458069629518985]
  We introduce power term algebra, a representation language for Boolean formulae designed to bridge conjunctive normal form (CNF) and algebraic normal form (ANF)<n>The language is motivated by the mismatch between these representations: direct CNF->ANF conversion may cause exponential blowup unless formulas are decomposed into smaller fragments, typically through auxiliary variables and side constraints.<n>Our framework addresses this mismatch within the representation itself, compactly encoding structured families of monomials while representing CNF clauses directly.
  arXiv  Detail & Related papers  (2026-03-14T09:22:52Z)
• 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)
• DivLogicEval: A Framework for Benchmarking Logical Reasoning Evaluation in Large Language Models [58.439517684779936]
  This paper proposes a new classical logic benchmark DivLogicEval, consisting of natural sentences composed of diverse statements in a counterintuitive way.<n>To ensure a more reliable evaluation, we also introduce a new evaluation metric that mitigates the influence of bias and randomness inherent in Large Language Models.
  arXiv  Detail & Related papers  (2025-09-19T04:40:46Z)
• Fuzzy Propositional Formulas under the Stable Model Semantics [7.052794276153519]
  We define a stable model semantics for fuzzy propositional formulas, which generalizes both fuzzy propositional logic and the stable model semantics of classical propositional formulas.<n>The syntax of the language is the same as the syntax of fuzzy propositional logic, but its semantics distinguishes stable models from non-stable models.
  arXiv  Detail & Related papers  (2025-06-15T10:38:56Z)
• Disambiguate First Parse Later: Generating Interpretations for Ambiguity Resolution in Semantic Parsing [56.82807063333088]
  We propose a modular approach that resolves ambiguity using natural language interpretations before mapping these to logical forms. Our approach improves interpretation coverage and generalizes across datasets with different annotation styles, database structures, and ambiguity types.
  arXiv  Detail & Related papers  (2025-02-25T18:42:26Z)
• The Stable Model Semantics for Higher-Order Logic Programming [4.106754434769354]
  We propose a stable model semantics for higher-order logic programs. Our semantics is developed using Approximation Fixpoint Theory (AFT), a powerful formalism. We provide examples in different application domains, which demonstrate that higher-order logic programming under the stable model semantics is a powerful and versatile formalism.
  arXiv  Detail & Related papers  (2024-08-20T06:03:52Z)
• Past-present temporal programs over finite traces [1.4835015204811504]
  We study the so-called past-present syntactic subclass, which consists of a set of logic programming rules whose body references to the past and head to the present. We extend the definitions of completion and loop formulas to the case of past-present formulas, which allows capturing the temporal stable models of a set of past-present temporal programs.
  arXiv  Detail & Related papers  (2023-07-24T08:50:12Z)
• Semantic Role Labeling Meets Definition Modeling: Using Natural Language to Describe Predicate-Argument Structures [104.32063681736349]
  We present an approach to describe predicate-argument structures using natural language definitions instead of discrete labels. Our experiments and analyses on PropBank-style and FrameNet-style, dependency-based and span-based SRL also demonstrate that a flexible model with an interpretable output does not necessarily come at the expense of performance.
  arXiv  Detail & Related papers  (2022-12-02T11:19:16Z)
• Hierarchical Phrase-based Sequence-to-Sequence Learning [94.10257313923478]
  We describe a neural transducer that maintains the flexibility of standard sequence-to-sequence (seq2seq) models while incorporating hierarchical phrases as a source of inductive bias during training and as explicit constraints during inference. Our approach trains two models: a discriminative derivation based on a bracketing grammar whose tree hierarchically aligns source and target phrases, and a neural seq2seq model that learns to translate the aligned phrases one-by-one.
  arXiv  Detail & Related papers  (2022-11-15T05:22:40Z)
• Benchmarking Language Models for Code Syntax Understanding [79.11525961219591]
  Pre-trained language models have demonstrated impressive performance in both natural language processing and program understanding. In this work, we perform the first thorough benchmarking of the state-of-the-art pre-trained models for identifying the syntactic structures of programs. Our findings point out key limitations of existing pre-training methods for programming languages, and suggest the importance of modeling code syntactic structures.
  arXiv  Detail & Related papers  (2022-10-26T04:47:18Z)
• Learning to Reason With Relational Abstractions [65.89553417442049]
  We study how to build stronger reasoning capability in language models using the idea of relational abstractions. We find that models that are supplied with such sequences as prompts can solve tasks with a significantly higher accuracy.
  arXiv  Detail & Related papers  (2022-10-06T00:27:50Z)
• Rationale-Augmented Ensembles in Language Models [53.45015291520658]
  We reconsider rationale-augmented prompting for few-shot in-context learning. We identify rationale sampling in the output space as the key component to robustly improve performance. We demonstrate that rationale-augmented ensembles achieve more accurate and interpretable results than existing prompting approaches.
  arXiv  Detail & Related papers  (2022-07-02T06:20:57Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Foundations of Symbolic Languages for Model Interpretability [2.3361634876233817]
  We study the computational complexity of FOIL queries over two classes of ML models often deemed to be easily interpretable. We present a prototype implementation of FOIL wrapped in a high-level declarative language.
  arXiv  Detail & Related papers  (2021-10-05T21:56:52Z)
• A Logical Characterization of the Preferred Models of Logic Programs with Ordered Disjunction [1.7403133838762446]
  We provide a novel, model-theoretic semantics for Logic Programs with Ordered Disjunction (LPODs) We demonstrate that the proposed approach overcomes the shortcomings of the traditional semantics of LPODs. New approach can be used to define the semantics of a natural class of logic programs that can have both ordered and classical disjunctions in the heads of clauses.
  arXiv  Detail & Related papers  (2021-08-07T05:36:12Z)
• 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)

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.