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
• Authors: Ahmad-Saher Azizi-Sultan
• 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

• 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.