© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

Sequent Calculus and Quantum Parallelism

Giulia Battilotti

Published Jan 7, 2015• 0 citations

Abstract

In the last years, quantum computational logics have been developed in order to describe the logical setting of quantum computation [1]. An important challenge is the development of proof theoretical tools for quantum computation, so that the physical process of computation can correspond to a logical process of computation. In particular, the challenge is that quantum computational speed up, due to superposition and entanglement, can find an explanation in terms of logical proofs. The object of our research is a sequent calculus developed in the framework of basic logic, that is a logical platform to study extensional logics, including quantum logics [2, 3]. In basic logic, logical connectives and their rules are the result of importing suitable links at the metalevel into the object level. We suppose that a particular kind of dynamics between the object level and the metalevel is created when considering a quantum system rather than a classical one. This is due to a specific treatment of variables, that, in our view, can create the logical setting for a holistic, rather than compositional, treatment of information, proper of entangled states [4]. Then we develop a predicative sequent calculus. In it, superposition is built by quantifying a propo-sition, associated with a quantum system, on a first order domain determined by the experiments on such system. Then a convenient treatment of variables can create dynamically entangled states in logical

Related papers

Sequent Calculus Representations for Quantum Circuits

Cameron Beebe

When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.

arXiv:1606.06799•Electronic Proceedings in Theoretical Computer Science•Jun 20, 2016•0 citations

1BASIC LOGIC AND QUANTUM ENTANGLEMENT

P. A. Zizzi

As it is well known, quantum entanglement is one of the most important features of quantum computing, as it leads to massive quantum parallelism, hence to exponential computational speed-up. In a sense, quantum entanglement is considered as an implicit property of quantum computation itself. But...can it be made explicit? In other words, is it possible to find the connective "entanglement" in a logical sequent calculus for the machine language? And also, is it possible to "teach" the quantum computer to "mimic" the EPR "paradox"? The answer is in the affirmative, if the logical sequent calculus is that of the weakest possible logic, namely Basic logic. A weak logic has few structural rules. But in logic, a weak structure leaves more room for connectives (for example the connective "entanglement"). Furthermore, the absence in Basic logic of the two structural rules of contraction and weakening corresponds to the validity of the no-cloning and no-erase theorems, respectively, in quantum computing.

•Nov 10, 2006•12 citations

From Quantum Metalanguage to the Logic of Qubits

Paola Zizzi

The main aim of this thesis is to look for a logical deductive calculus (we will adopt sequent calculus, originally introduced in Gentzen, 1935), which could describe quantum information and its properties. More precisely, we intended to describe in logical terms the formation of the qubit (the unit of quantum information) which is a particular linear superposition of the two classical bits 0 and 1. To do so, we had to introduce the new connective "quantum superposition", in the logic of one qubit, Lq, as the classical conjunction cannot describe this quantum link.

arXiv:1003.5976•Mar 31, 2010•14 citations

Basic logic and quantum entanglement

P A Zizzi

As it is well known, quantum entanglement is one of the most important features of quantum computing, as it leads to massive quantum parallelism, hence to exponential computational speed-up. In a sense, quantum entanglement is considered as an implicit property of quantum computation itself. But... can it be made explicit? In other words, is it possible to find the connective "entanglement" in a logical sequent calculus for the machine language? And also, is it possible to "teach" the quantum computer to "mimic" the EPR "paradox"? The answer is in the affirmative, if the logical sequent calculus is that of the weakest possible logic, namely Basic logic. - A weak logic has few structural rules. But in logic, a weak structure leaves more room for connectives (for example the connective "entanglement"). Furthermore, the absence in Basic logic of the two structural rules of contraction and weakening corresponds to the validity of the no-cloning and no-erase theorems, respectively, in quantum computing.

arXiv:quant-ph/0611119•Journal of Physics Conference Series•May 1, 2007•4 citations

Holistic logical arguments in quantum computation

María Luisa Dalla Chiara, Roberto Giuntini, Roberto Leporini +1 more

Abstract Quantum computational logics represent a logical abstraction from the circuit-theory in quantum computation. In these logics formulas are supposed to denote pieces of quantum information (qubits, quregisters or mixtures of quregisters), while logical connectives correspond to (quantum logical) gates that transform quantum information in a reversible way. The characteristic holistic features of the quantum theoretic formalism (which play an essential role in entanglement-phenomena) can be used in order to develop a holistic version of the quantum computational semantics. In contrast with the compositional character of most standard semantic approaches, meanings of formulas are here dealt with as global abstract objects that determine the contextual meanings of the formulas’ components (from the whole to the parts). We present a survey of the most significant logical arguments that are valid or that are possibly violated in the framework of this semantics. Some logical features that may appear prima facie strange seem to reflect pretty well informal arguments that are currently used in our rational activity.

arXiv:1602.07516•Mathematica Slovaca•Apr 1, 2016•4 citations

Holistic logical arguments in quantum computation

Leporini, Roberto

Quantum computational logics represent a logical abstraction from the circuit-theory in quantum computation. In these logics formulas are supposed to denote pieces of quantum information (qubits, quregisters or mixtures of quregisters), while logical connectives correspond to (quantum logical) gates that transform quantum information in a reversible way. The characteristic holistic features of the quantum theoretic formalism (which play an essential role in entanglement-phenomena) can be used in order to develop a holistic version of the quantum computational semantics. In contrast with the compositional character of most standard semantic approaches, meanings of formulas are here dealt with as global abstract objects that determine the contextual meanings of the formulas' components (from the whole to the parts). We present a survey of the most significant logical arguments that are valid or that are possibly violated in the framework of this semantics. Some logical features that may appear prima facie strange seem to reflect pretty well informal arguments that are currently used in our rational activity.

•Jan 1, 2016•18 citations

In the last years, quantum computational logics have been developed in order to describe the logical setting of quantum computation [1]. An important challenge is the development of proof theoretical tools for quantum computation, so that the physical process of computation can correspond to a logical process of computation. In particular, the challenge is that quantum computational speed up, due to superposition and entanglement, can find an explanation in terms of logical proofs. The object of our research is a sequent calculus developed in the framework of basic logic, that is a logical platform to study extensional logics, including quantum logics [2, 3]. In basic logic, logical connectives and their rules are the result of importing suitable links at the metalevel into the object level. We suppose that a particular kind of dynamics between the object level and the metalevel is created when considering a quantum system rather than a classical one. This is due to a specific treatment of variables, that, in our view, can create the logical setting for a holistic, rather than compositional, treatment of information, proper of entangled states [4]. Then we develop a predicative sequent calculus. In it, superposition is built by quantifying a propo-sition, associated with a quantum system, on a first order domain determined by the experiments on such system. Then a convenient treatment of variables can create dynamically entangled states in logical

When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.

As it is well known, quantum entanglement is one of the most important features of quantum computing, as it leads to massive quantum parallelism, hence to exponential computational speed-up. In a sense, quantum entanglement is considered as an implicit property of quantum computation itself. But...can it be made explicit? In other words, is it possible to find the connective "entanglement" in a logical sequent calculus for the machine language? And also, is it possible to "teach" the quantum computer to "mimic" the EPR "paradox"? The answer is in the affirmative, if the logical sequent calculus is that of the weakest possible logic, namely Basic logic. A weak logic has few structural rules. But in logic, a weak structure leaves more room for connectives (for example the connective "entanglement"). Furthermore, the absence in Basic logic of the two structural rules of contraction and weakening corresponds to the validity of the no-cloning and no-erase theorems, respectively, in quantum computing.

The main aim of this thesis is to look for a logical deductive calculus (we will adopt sequent calculus, originally introduced in Gentzen, 1935), which could describe quantum information and its properties. More precisely, we intended to describe in logical terms the formation of the qubit (the unit of quantum information) which is a particular linear superposition of the two classical bits 0 and 1. To do so, we had to introduce the new connective "quantum superposition", in the logic of one qubit, Lq, as the classical conjunction cannot describe this quantum link.

As it is well known, quantum entanglement is one of the most important features of quantum computing, as it leads to massive quantum parallelism, hence to exponential computational speed-up. In a sense, quantum entanglement is considered as an implicit property of quantum computation itself. But... can it be made explicit? In other words, is it possible to find the connective "entanglement" in a logical sequent calculus for the machine language? And also, is it possible to "teach" the quantum computer to "mimic" the EPR "paradox"? The answer is in the affirmative, if the logical sequent calculus is that of the weakest possible logic, namely Basic logic. - A weak logic has few structural rules. But in logic, a weak structure leaves more room for connectives (for example the connective "entanglement"). Furthermore, the absence in Basic logic of the two structural rules of contraction and weakening corresponds to the validity of the no-cloning and no-erase theorems, respectively, in quantum computing.

Abstract Quantum computational logics represent a logical abstraction from the circuit-theory in quantum computation. In these logics formulas are supposed to denote pieces of quantum information (qubits, quregisters or mixtures of quregisters), while logical connectives correspond to (quantum logical) gates that transform quantum information in a reversible way. The characteristic holistic features of the quantum theoretic formalism (which play an essential role in entanglement-phenomena) can be used in order to develop a holistic version of the quantum computational semantics. In contrast with the compositional character of most standard semantic approaches, meanings of formulas are here dealt with as global abstract objects that determine the contextual meanings of the formulas’ components (from the whole to the parts). We present a survey of the most significant logical arguments that are valid or that are possibly violated in the framework of this semantics. Some logical features that may appear prima facie strange seem to reflect pretty well informal arguments that are currently used in our rational activity.

Quantum computational logics represent a logical abstraction from the circuit-theory in quantum computation. In these logics formulas are supposed to denote pieces of quantum information (qubits, quregisters or mixtures of quregisters), while logical connectives correspond to (quantum logical) gates that transform quantum information in a reversible way. The characteristic holistic features of the quantum theoretic formalism (which play an essential role in entanglement-phenomena) can be used in order to develop a holistic version of the quantum computational semantics. In contrast with the compositional character of most standard semantic approaches, meanings of formulas are here dealt with as global abstract objects that determine the contextual meanings of the formulas' components (from the whole to the parts). We present a survey of the most significant logical arguments that are valid or that are possibly violated in the framework of this semantics. Some logical features that may appear prima facie strange seem to reflect pretty well informal arguments that are currently used in our rational activity.