Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

International Journal of Quantum Information

A LOGIC FOR QUANTUM COMPUTATION AND CLASSICAL SIMULATION OF QUANTUM ALGORITHMS

Manas K. Patra

Published Apr 1, 2008• 1 citation
Publisher

Abstract

The semantics of a language for reasoning about finite-dimensional quantum systems is presented. This language can express most important classes of assertions about quantum systems, including formulas for outputs of all combinational quantum circuits/algorithms. The main result of this paper is an algorithm for efficient translation of a formula of language into an equivalent formula in another decidable language ℝℂ, which is the language of reals and its complex extension. An important consequence is a descriptive characterization of quantum circuits that can be efficiently simulated classically. We illustrate this with examples of two classes of quantum circuits which are known to have efficient classical simulation. The algorithm for deciding the satisfiability of a general formula can be adapted for the simulation.

DOI
10.1142/s0219749908003554

Related papers

Towards Quantum Logic Programming

Giovanni Pilato, Filippo Vella, Tommaso Brugarino +1 more

The advantages of quantum computing have been demonstrated across many application fields, and the development of increasingly powerful hardware platforms is enabling wider adoption of quantum solutions in real-world tasks. However, a significant limitation to applying the quantum paradigm to real problems is the difficulty in designing solutions using quantum computational blocks. We illustrate an innovative approach that allows for the description of a solution using a high-level language, which can be translated into a set of appropriate quantum gates to perform the desired computation. We present a system based on quantum computational logic proposed by Dalla Chiara et al. to represent a quantum computation within a Prolog environment. In this system, a logic formula is translated into a quantum-operable formulation, following the logic’s holistic semantics. Preliminary examples illustrate the method’s application.

IEEE Conference on Pervasive and Intelligent Computing (PICom)•Oct 21, 2025•0 citations

LOGICS FROM QUANTUM COMPUTATION WITH BOUNDED ADDITIVE OPERATORS

Cesarino Bertini, Roberto Leporini

The theory of gates in quantum computation has suggested new forms of quantum logic, called quantum computational logics, where the meaning of a sentence is identified with a system of qubits in a pure or, more generally, mixed state. In this framework, any formula of the language gives rise to a quantum circuit that transforms the state associated to the atomic subformulas into the state associated to the formula and vice versa. On this basis, some holistic semantic situations can be described, where the meaning of whole determines the meaning of the parts, by non-linear and anti-unitary operators. We prove that the semantics with such operators and the semantics with unitary operators turn out to characterize the same logic.

International Journal of Quantum Information•Apr 1, 2012•3 citations

Algebraic language for the efficient representation and optimization of quantum circuits

Daniel Escánez-Expósito, Pino Caballero‐Gil, Marcos Rodriguez-Vega +2 more

Abstract The use of graphical language in quantum computing for the representation of algorithms, although intuitive, is not very useful for different tasks such as the description of quantum circuits in text environments, the calculation of quantum states or the optimization of quantum circuits. While classical circuits can be represented either by circuit graphs or by Boolean expressions, quantum circuits have until now predominantly been illustrated as circuit graphs because no formal language for quantum circuits that allows algebraic manipulations has so far been accepted. This work proposes a means to represent quantum circuits in a convenient and concise manner, similar to the way Boolean expressions are used in classical circuits. The proposed notation allows the consistent and parameterized description of quantum algorithms, as well as the easy handling of the elements that compose it to achieve powerful optimizations in the number of gates of the circuits. To visualize it, a software implementation of an algebraic quantum circuit framework has been made, which allows describing quantum circuits, as well as their respective state vectors, using the proposed algebraic language.

Physica Scripta•Dec 16, 2024•4 citations

Automated Theorem Proving for Quantum Circuit Verification using SAT Solvers

Jincheng Zhang

The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.

•Sep 5, 2026•0 citations

Using HDLs for describing quantum circuits

Mihai Udrescu, Lucian Prodan, Mircea Vlăduţiu

The quantum algorithms could efficiently solve problems having exponential classical solutions [8]. The circuit model is considered as the most feasible implementation of the quantum algorithms [17]. This paper tries to find common ground between classical circuit design techniques and quantum computation, by identifying quantum circuit specification and simulation tools under the form of Hardware Description Languages (HDLs). The HDL-based simulation approach could reduce the complexity of quantum circuit simulation, by considering entanglement as the main source of gate-level simulation complexity, and isolating it in an automated manner. This is possible by taking advantage of the HDL feature of describing a circuit with both structural and functional architectures. We also performed an analysis of our methodology effectiveness, for the arithmetic circuits involved in Shor's algorithm and the circuits implementing Grover's algorithm. Our method is further improved by an entangled representation avoidance technique called 'bubble logic insertion'.

ACM International Conference on Computing Frontiers (CF)•Apr 14, 2004•24 citations

A Lambda Calculus for Quantum Computation

André van Tonder

The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of linear logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.

arXiv:quant-ph/0307150•SIAM Journal on Computing•Jan 1, 2004•196 citations
The semantics of a language for reasoning about finite-dimensional quantum systems is presented. This language can express most important classes of assertions about quantum systems, including formulas for outputs of all combinational quantum circuits/algorithms. The main result of this paper is an algorithm for efficient translation of a formula of language into an equivalent formula in another decidable language ℝℂ, which is the language of reals and its complex extension. An important consequence is a descriptive characterization of quantum circuits that can be efficiently simulated classically. We illustrate this with examples of two classes of quantum circuits which are known to have efficient classical simulation. The algorithm for deciding the satisfiability of a general formula can be adapted for the simulation.
The advantages of quantum computing have been demonstrated across many application fields, and the development of increasingly powerful hardware platforms is enabling wider adoption of quantum solutions in real-world tasks. However, a significant limitation to applying the quantum paradigm to real problems is the difficulty in designing solutions using quantum computational blocks. We illustrate an innovative approach that allows for the description of a solution using a high-level language, which can be translated into a set of appropriate quantum gates to perform the desired computation. We present a system based on quantum computational logic proposed by Dalla Chiara et al. to represent a quantum computation within a Prolog environment. In this system, a logic formula is translated into a quantum-operable formulation, following the logic’s holistic semantics. Preliminary examples illustrate the method’s application.
The theory of gates in quantum computation has suggested new forms of quantum logic, called quantum computational logics, where the meaning of a sentence is identified with a system of qubits in a pure or, more generally, mixed state. In this framework, any formula of the language gives rise to a quantum circuit that transforms the state associated to the atomic subformulas into the state associated to the formula and vice versa. On this basis, some holistic semantic situations can be described, where the meaning of whole determines the meaning of the parts, by non-linear and anti-unitary operators. We prove that the semantics with such operators and the semantics with unitary operators turn out to characterize the same logic.
Abstract The use of graphical language in quantum computing for the representation of algorithms, although intuitive, is not very useful for different tasks such as the description of quantum circuits in text environments, the calculation of quantum states or the optimization of quantum circuits. While classical circuits can be represented either by circuit graphs or by Boolean expressions, quantum circuits have until now predominantly been illustrated as circuit graphs because no formal language for quantum circuits that allows algebraic manipulations has so far been accepted. This work proposes a means to represent quantum circuits in a convenient and concise manner, similar to the way Boolean expressions are used in classical circuits. The proposed notation allows the consistent and parameterized description of quantum algorithms, as well as the easy handling of the elements that compose it to achieve powerful optimizations in the number of gates of the circuits. To visualize it, a software implementation of an algebraic quantum circuit framework has been made, which allows describing quantum circuits, as well as their respective state vectors, using the proposed algebraic language.
The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.
The quantum algorithms could efficiently solve problems having exponential classical solutions [8]. The circuit model is considered as the most feasible implementation of the quantum algorithms [17]. This paper tries to find common ground between classical circuit design techniques and quantum computation, by identifying quantum circuit specification and simulation tools under the form of Hardware Description Languages (HDLs). The HDL-based simulation approach could reduce the complexity of quantum circuit simulation, by considering entanglement as the main source of gate-level simulation complexity, and isolating it in an automated manner. This is possible by taking advantage of the HDL feature of describing a circuit with both structural and functional architectures. We also performed an analysis of our methodology effectiveness, for the arithmetic circuits involved in Shor's algorithm and the circuits implementing Grover's algorithm. Our method is further improved by an entangled representation avoidance technique called 'bubble logic insertion'.
The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of linear logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.