Partial Orders, Residuation, and First-Order Linear Logic

• URL: http://arxiv.org/abs/2008.06351v1
• Date: Fri, 14 Aug 2020 13:06:21 GMT
• Title: Partial Orders, Residuation, and First-Order Linear Logic
• Authors: Richard Moot
• Abstract summary: We will show that adding partial order constraints in such a way as each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators.
• Score: 0.20305676256390934
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We will investigate proof-theoretic and linguistic aspects of first-order linear logic. We will show that adding partial order constraints in such a way that each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators. In addition, the partial order constraints improve the efficiency of proof search.

Related papers

• Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning [28.111458981621105]
  Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short. We propose a Compositional First-Order Logic Translation to capture logical semantics hidden in the natural language during translation. We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches.
  arXiv  Detail & Related papers  (2024-10-10T15:42:39Z)
• 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)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  Two lines of approaches are adopted for complex reasoning with LLMs. One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps. The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers. We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
  arXiv  Detail & Related papers  (2023-11-16T11:26:21Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  In general,fMT was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics) with a tableau-based semi-decision procedure. We show that for anyfMT formula satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with a new rule is also guaranteed to terminate.
  arXiv  Detail & Related papers  (2023-07-31T17:02:23Z)
• 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)
• Linearization Algorithms for Fully Composite Optimization [61.20539085730636]
  This paper studies first-order algorithms for solving fully composite optimization problems convex compact sets. We leverage the structure of the objective by handling differentiable and non-differentiable separately, linearizing only the smooth parts.
  arXiv  Detail & Related papers  (2023-02-24T18:41:48Z)
• Linear Partial Monitoring for Sequential Decision-Making: Algorithms, Regret Bounds and Applications [70.67112733968654]
  Partial monitoring is an expressive framework for sequential decision-making. We present a simple and unified analysis of partial monitoring, and further extend the model to the contextual and kernelized setting.
  arXiv  Detail & Related papers  (2023-02-07T18:58:25Z)
• On Parsing as Tagging [66.31276017088477]
  We show how to reduce tetratagging, a state-of-the-art constituency tagger, to shift--reduce parsing. We empirically evaluate our taxonomy of tagging pipelines with different choices of linearizers, learners, and decoders.
  arXiv  Detail & Related papers  (2022-11-14T13:37:07Z)
• Uncertain Linear Logic via Fibring of Probabilistic and Fuzzy Logic [0.0]
  probabilistic and fuzzy logic correspond to two different assumptions regarding the combination of propositions whose evidence bases are not currently available. It is shown that these two sets of formulas provide a natural grounding for the multiplicative and additive operator-sets in linear logic. The concept of linear logic as a logic of resources" is manifested here via the principle of conservation of evidence"
  arXiv  Detail & Related papers  (2020-09-28T00:19:42Z)
• Deriving Theorems in Implicational Linear Logic, Declaratively [0.0]
  We show how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. As applications, we generate datasets for correctness and scalability testing of linear logic theorem provers and training data for neural networks working on theorem proving challenges.
  arXiv  Detail & Related papers  (2020-09-22T00:48:45Z)
• 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.