Resolution for Constrained Pseudo-Propositional Logic

• URL: http://arxiv.org/abs/2306.06630v1
• Date: Sun, 11 Jun 2023 09:17:24 GMT
• Title: Resolution for Constrained Pseudo-Propositional Logic
• Abstract summary: This work shows how propositional resolution can be generalized to obtain a resolution proof system for constrained pseudo-propositional logic. Unlike the construction of CNF formulas which are restricted to a finite set of clauses, the extended CPPL does not require the corresponding set to be finite.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This work, shows how propositional resolution can be generalized to obtain a resolution proof system for constrained pseudo-propositional logic (CPPL), which is an extension resulted from inserting the natural numbers with few constraints symbols into the alphabet of propositional logic and adjusting the underling language accordingly. Unlike the construction of CNF formulas which are restricted to a finite set of clauses, the extended CPPL does not require the corresponding set to be finite. Although this restriction is made dispensable, this work presents a constructive proof showing that the generalized resolution for CPPL is sound and complete. As a marginal result, this implies that propositional resolution is also sound and complete for formulas with even infinite set of clauses.

Related papers

• Foundations of MT-PDCL: Measure-Theoretic Probabilistic Definite Clause Logic [0.0]
  We introduce Measure-Theoretic Probabilistic Definite Clause Logic.<n>It eliminates the finite-domain restriction by defining variables over bounded index domains.<n>It unifies the integration of continuous distributions with the evaluation of exact continuous observations.
  arXiv  Detail & Related papers  (2026-08-13T09:43:33Z)
• 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)
• Text-to-State Mapping for Non-Resolution Reasoning: The Contradiction-Preservation Principle [0.0]
  Non-Resolution Reasoning (NRR) provides a formal framework for maintaining semantic ambiguity rather than forcing premature interpretation collapse.<n>This paper introduces the text-to-state mapping function that transforms linguistic input into superposition states within the NRR framework.
  arXiv  Detail & Related papers  (2026-01-12T08:04:47Z)
• On the Complexity of the Grounded Semantics for Infinite Argumentation Frameworks [0.0]
  We use methods from mathematical logic, specifically computability and set theory, to analyze the grounded extension.<n>Finding this fixed-point requires transfinite iterations.<n>This shows a marked distinction from the finite case where the grounded extension is-time computable.
  arXiv  Detail & Related papers  (2025-11-27T12:13:30Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• A Unifying Framework for Semiring-Based Constraint Logic Programming With Negation (full version) [5.911540700785975]
  Constraint Logic Programming (CLP) is a logic programming formalism used to solve problems requiring the consideration of constraints.<n>We investigate an extension of CLP which unifies many extensions and allows negation in the body.
  arXiv  Detail & Related papers  (2025-07-21T21:04:03Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  We propose that guiding models to perform a systematic and comprehensive reasoning process allows models to execute much finer-grained and accurate entailment decisions.<n>We define a 3-step reasoning process, consisting of (i) claim decomposition, (ii) sub-claim attribution and entailment classification, and (iii) aggregated classification, showing that such guided reasoning indeed yields improved hallucination detection.
  arXiv  Detail & Related papers  (2025-06-05T17:02:52Z)
• Constrained Language Generation with Discrete Diffusion Models [61.81569616239755]
  We present Constrained Discrete Diffusion (CDD), a novel method for enforcing constraints on natural language by integrating discrete diffusion models with differentiable optimization. We show how this technique can be applied to satisfy a variety of natural language constraints, including (i) toxicity mitigation by preventing harmful content from emerging, (ii) character and sequence level lexical constraints, and (iii) novel molecule sequence generation with specific property adherence.
  arXiv  Detail & Related papers  (2025-03-12T19:48:12Z)
• Strong Equivalence in Answer Set Programming with Constraints [8.096489007229774]
  Two groups of rules are considered strongly equivalent if, informally speaking, they have the same meaning in any context. We show that strong equivalence can be precisely characterized by their equivalence in the logic of Here-and-There with constraints. We present a translation from the language of several clingo-based answer set solvers that handle constraints into the language of Here-and-There with constraints.
  arXiv  Detail & Related papers  (2025-02-06T18:43:59Z)
• A novel framework for systematic propositional formula simplification based on existential graphs [1.104960878651584]
  This paper presents a novel simplification calculus for propositional logic derived from Peirce's existential graphs' rules of inference and implication graphs. Our rules can be applied to propositional logic formulae in nested form, are equivalence-preserving, guarantee a monotonically decreasing number of variables, clauses and literals, and maximise the preservation of structural problem information.
  arXiv  Detail & Related papers  (2024-05-27T11:42:46Z)
• Qubit Number Optimization for Restriction Terms of QUBO Hamiltonians [62.997667081978825]
  It is mathematically allowed to ask for fractional values of $R$. We show how they can reduce the number of qubits needed to implement the restriction hamiltonian even further. Finally, we characterize the response of DWave's Advantage$_$system4.1 Quantum Annealer (QA) when faced with the implementation of FRCs.
  arXiv  Detail & Related papers  (2023-06-12T08:25:56Z)
• Range-Restricted Interpolation through Clausal Tableaux [0.0]
  We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP.
  arXiv  Detail & Related papers  (2023-06-06T10:42:40Z)
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning [0.3867363075280543]
  We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering.
  arXiv  Detail & Related papers  (2023-05-22T11:12:39Z)
• Non-Deterministic Approximation Fixpoint Theory and Its Application in Disjunctive Logic Programming [11.215352918313577]
  Approximation fixpoint theory is a framework for studying the semantics of nonmonotonic logics. We extend AFT to dealing with non-deterministic constructs that allow to handle indefinite information. The applicability and usefulness of this generalization is illustrated in the context of disjunctive logic programming.
  arXiv  Detail & Related papers  (2022-11-30T18:58:32Z)
• 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)
• Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
  We present a framework for universal fault-tolerant logic motivated by the need for platform-independent logical gate definitions. We explore novel schemes for universal logic that improve resource overheads. Motivated by the favorable logical error rates for boundaryless computation, we introduce a novel computational scheme.
  arXiv  Detail & Related papers  (2021-12-22T19:00:03Z)
• Reinforcement Learning in Linear MDPs: Constant Regret and Representation Selection [136.4014229319618]
  We study the role of the representation of state-action value functions in regret minimization in finite-horizon Markov Decision Processes (MDPs) with linear structure. We first derive a necessary condition on the representation, called universally spanning optimal features (UNISOFT), to achieve constant regret in any MDP with linear reward function.
  arXiv  Detail & Related papers  (2021-10-27T22:07:08Z)
• Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
  We give a sound and strongly complete axiomatization that can be parametrized to cover essentially every real-valued logic. Our class of sentences are very rich, and each describes a set of possible real values for a collection of formulas of the real-valued logic.
  arXiv  Detail & Related papers  (2020-08-06T02:13:11Z)
• Modular Answer Set Programming as a Formal Specification Language [8.823761706435814]
  We study the problem of formal verification for Answer Set Programming (ASP) We obtain a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance.
  arXiv  Detail & Related papers  (2020-08-05T09:25:51Z)
• Conditional gradient methods for stochastically constrained convex minimization [54.53786593679331]
  We propose two novel conditional gradient-based methods for solving structured convex optimization problems. The most important feature of our framework is that only a subset of the constraints is processed at each iteration. Our algorithms rely on variance reduction and smoothing used in conjunction with conditional gradient steps, and are accompanied by rigorous convergence guarantees.
  arXiv  Detail & Related papers  (2020-07-07T21:26:35Z)

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.