Quantum automated theorem proving

• URL: http://arxiv.org/abs/2601.07953v1
• Date: Mon, 12 Jan 2026 19:39:33 GMT
• Title: Quantum automated theorem proving
• Authors: Zheng-Zhi Sun, Qi Ye, Dong-Ling Deng,
• Abstract summary: We propose a generic framework for quantum automated theorem proving.<n>We introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks.<n>We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic.
• Score: 15.134110328567838
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of applications and the quest for enhanced theorem-proving capabilities remains a prominent pursuit in artificial intelligence. Here, we propose a generic framework for quantum automated theorem proving, where the intrinsic quantum superposition and entanglement features would lead to potential advantages. In particular, we introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks. We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic with quadratically reduced query complexity. In addition, we propose the quantum algebraic proving method for geometric theorems, extending Wu's algebraic approach beyond the classical setting. Through concrete examples, including geometry problems from the International Mathematical Olympiad, we demonstrate how a quantum computer may prove geometric theorems with quadratic better query complexity. Our results establish a primary approach towards building quantum automatic theorem provers, which would be crucial for practical applications of both near-term and future quantum technologies.

Related papers

• Formal Modeling and Verification of Grover's Algorithm [0.0]
  Grover's algorithm relies on the superposition and interference of quantum mechanics.<n>We formally model and verify Grover's algorithm in the HOL Light theorem prover.
  arXiv  Detail & Related papers  (2026-01-05T06:56:21Z)
• Symbolic Specification and Reasoning for Quantum Data and Operations [5.341843260877702]
  We present a general logical framework, called Operator Logic $mathbfSOL$, which enables symbolic specification and reasoning about quantum data and operations.<n>Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations.<n>This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data.
  arXiv  Detail & Related papers  (2025-12-26T20:57:42Z)
• A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics [6.445494669467905]
  We use duality theorems for countable probability distributions and finite-dimensional quantum states to build relational program logics for classical-quantum programs.<n>We establish soundness and completeness of a new relational program logic, called $mathsfcqOTL$, for classical-quantum programs.
  arXiv  Detail & Related papers  (2025-10-08T14:19:03Z)
• Artificial intelligence for representing and characterizing quantum systems [49.29080693498154]
  Efficient characterization of large-scale quantum systems is a central challenge in quantum science.<n>Recent advances in artificial intelligence (AI) have emerged as a powerful tool to address this challenge.<n>This review discusses how each of these AI paradigms contributes to two core tasks in quantum systems characterization.
  arXiv  Detail & Related papers  (2025-09-05T08:41:24Z)
• A mathematical model for a universal digital quantum computer with an application to the Grover-Rudolph algorithm [0.0]
  We develop a novel framework for universal digital quantum computation using algebraic probability theory.<n>We define quantum circuits as finite sequences of elementary quantum gates.<n>We design a quantum circuit that approximates a given probability density function.
  arXiv  Detail & Related papers  (2025-03-17T17:18:45Z)
• QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
  Quantum computing is recognized for the significant speedup it offers over classical computing through quantum algorithms.<n>QCircuitBench is the first benchmark dataset designed to evaluate AI's capability in designing and implementing quantum algorithms.
  arXiv  Detail & Related papers  (2024-10-10T14:24:30Z)
• Quantum algorithms: A survey of applications and end-to-end complexities [88.57261102552016]
  The anticipated applications of quantum computers span across science and industry.<n>We present a survey of several potential application areas of quantum algorithms.<n>We outline the challenges and opportunities in each area in an "end-to-end" fashion.
  arXiv  Detail & Related papers  (2023-10-04T17:53:55Z)
• No-signalling constrains quantum computation with indefinite causal structure [45.279573215172285]
  We develop a formalism for quantum computation with indefinite causal structures. We characterize the computational structure of higher order quantum maps. We prove that these rules, which have a computational and information-theoretic nature, are determined by the more physical notion of the signalling relations between the quantum systems.
  arXiv  Detail & Related papers  (2022-02-21T13:43:50Z)
• Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra [11.078562853984211]
  We investigate the reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. Key features of KAT including the idempotent law and the nice properties of classical tests fail to hold in the context of quantum programs. We propose Non-idempotent Kleene Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA.
  arXiv  Detail & Related papers  (2021-10-13T20:27:01Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify quantum advantage of an untrusted prover. In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits.
  arXiv  Detail & Related papers  (2021-07-05T17:45:41Z)

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.