A Coq Formalization of Unification Modulo Exclusive-Or

• URL: http://arxiv.org/abs/2502.09225v1
• Date: Thu, 13 Feb 2025 11:51:37 GMT
• Title: A Coq Formalization of Unification Modulo Exclusive-Or
• Authors: Yichi Xu, Daniel J. Dougherty, Rose Bohrer,
• Abstract summary: We focus on XOR-Unification, that is, unification modulo the theory of exclusive-or.<n>In the proof assistant Coq, we implement an algorithm that solves XOR unification problems.<n>We obtain an implementation in the programming language OCaml.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems, whose design was inspired by Liu and Lynch, and prove it sound, complete, and terminating. Using Coq's code extraction capability we obtain an implementation in the programming language OCaml.

Related papers

• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps. We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths. SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• Critical Thinking: Which Kinds of Complexity Govern Optimal Reasoning Length? [72.70486097967124]
  We formalize a framework using deterministic finite automata (DFAs) We show that there exists an optimal amount of reasoning tokens such that the probability of producing a correct solution is maximized. We then demonstrate an implication of these findings: being able to predict the optimal number of reasoning tokens for new problems and filtering out non-optimal length answers results in consistent accuracy improvements.
  arXiv  Detail & Related papers  (2025-04-02T17:45:58Z)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL is a formal verified EL++ reasoner equipped with machine-checkable correctness proofs.<n>Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.
  arXiv  Detail & Related papers  (2024-12-11T19:17:28Z)
• Mitigating Misleading Chain-of-Thought Reasoning with Selective Filtering [59.495717939664246]
  Large language models have manifested remarkable capabilities by leveraging chain-of-thought (CoT) reasoning techniques to solve intricate questions. We propose a novel approach called the selective filtering reasoner (SelF-Reasoner) that assesses the entailment relationship between the question and the candidate reasoning chain. SelF-Reasoner improves the fine-tuned T5 baseline consistently over the ScienceQA, ECQA, and LastLetter tasks.
  arXiv  Detail & Related papers  (2024-03-28T06:28:35Z)
• 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)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions [0.0]
  We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions. As usual in synthetic approaches, we employ a definition of oracle computations based on meta-level functions. We show that Turing reducibility forms an upper semilattice, transports decidability, and is strictly more expressive than truth-table reducibility.
  arXiv  Detail & Related papers  (2023-07-28T13:16:46Z)
• A Formalization of Operads in Coq [0.0]
  In this paper, we discuss our formalization of an operad in the proof assistant Coq. Coq provides a formal mathematical basis for our meta-language development within V-SPELLS. Our work also provides, to our knowledge, the first known formalization of operads within a proof assistant that has significant automation.
  arXiv  Detail & Related papers  (2023-03-15T19:29:40Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens [0.7614628596146599]
  We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. We give a full classification of FSAT depending on the first-order signature of non-logical symbols. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability.
  arXiv  Detail & Related papers  (2021-04-29T16:05:31Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)
• Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory [0.0]
  We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. We give a full classification of FSAT depending on the first-order signature of non-logical symbols. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.
  arXiv  Detail & Related papers  (2020-04-15T23:26:04Z)

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.