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. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems. We obtain an implementation in the programming language OCaml.
• Score: 0.0
• License:
• 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

• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL is a formal verified EL++ reasoner equipped with machine-checkable correctness proofs. 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)
• 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)
• Complex Query Answering on Eventuality Knowledge Graph with Implicit Logical Constraints [48.831178420807646]
  We propose a new framework to leverage neural methods to answer complex logical queries based on an EVentuality-centric KG. Complex Eventuality Query Answering (CEQA) considers the implicit logical constraints governing the temporal order and occurrence of eventualities. We also propose a Memory-Enhanced Query (MEQE) to significantly improve the performance of state-of-the-art neural query encoders on the CEQA task.
  arXiv  Detail & Related papers  (2023-05-30T14:29:24Z)
• 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)
• Constrained mixers for the quantum approximate optimization algorithm [55.41644538483948]
  We present a framework for constructing mixing operators that restrict the evolution to a subspace of the full Hilbert space. We generalize the "XY"-mixer designed to preserve the subspace of "one-hot" states to the general case of subspaces given by a number of computational basis states. Our analysis also leads to valid Trotterizations for "XY"-mixer with fewer CX gates than is known to date.
  arXiv  Detail & Related papers  (2022-03-11T17:19:26Z)
• 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.