Combining paraconsistent and dynamic logic for Qiskit

Abstract

This dissertation introduces a logic aimed at combining dynamic logic and paraconsistent logic for application to the quantum domain, to reason about quantum phase properties: Paraconsistent Phased Logic Of Quantum Programs (PhLQP◦ ). In the design PhLQP◦ , firstly the dynamic was built first, Phased Logic Of Quantum Programs (PhLQP). PhLQP is itself a dynamic logic capable of dealing with quantum phase properties, quantum measurements, unitary evolutions, and entanglements in compound systems , since it is a redesign of the already existing Logic Of Quantum Programs (LQP), [14], over a representation of quantum states restricted to a space B equipped with only two computational basis, standard and Hadamard. As instances of applications of the logic PhLQP, there is a formal proof of the correctness of the Quantum Teleportation Protocol, of the 2-party and 4-party of the Quantum Leader Election (QLE) protocol, and of the Quantum Fourier Transform (QFT) operator for 1, 2 and 3 qubits . On a second stage, PhLQP was extended with the connective ◦ known as the consistency operator, a typical connective of the paraconsistent logics Logics of Formal Inconsistency (LFIs), [8, 21, 22]. The definition of consistent quantum state and a set of proper para consistent axioms for the quantum domain, Fundamental Paraconsistent Quantum Axioms (FParQAxs), were provided. An example of application of PhLQP◦ is the possibility of express and prove correctness of the universal quantum gate, the Deustch gate.

Esta dissertação introduz uma lógica que tem como objectivo combinar lógica dinâmica e lógica paraconsistente com aplicação no domínio quântico, assim como expressar propriedades relacionadas com fases quânticas: PhLQP◦. No projetar da PhLQP◦, primeiramente concebeu-se a sua componente dinâmica, PhLQP. PhLQP por si só é uma lógica capaz de lidar com propriedades de fases quânticas, evoluções unitárias, e entrelaçamento em sistemas compostos, uma vez que é um redesenhar da já existente LQP, [14], sobre uma representação de estados quânticos restrita a um espaço B munido de apenas duas bases computacionais, standard e Hadamard. Como instâncias de aplicação da lógica PhLQP, há uma prova formal para a correção do protocolo de Teletransporte Quântico, para o protocolo QLE para uma party quer de 2 quer de 4 agentes, e para o operador de QFT de 1, 2, e 3 qubits. Numa segunda fase, PhLQP é extendida com a conectiva ◦, conhecida como operador de consistência, uma conectiva característica das LFIs, [8, 21, 22]. E a partir desta conectiva a definição de estado quântico consistente é um conjunto de axiomas paraconsistentes próprios para o domínio quântico, FParQAxs. Um exemplo de aplicação da PhLQP◦ é a possibilidade de expressar e permitir correção para o comportamento da gate quântica universal, a Deutsch-gate.