Quantum Algorithm for Multiplicative Linear Logic

  • Lorenzo Saraiva PUC-Rio
  • Edward Hermann Haeusler PUC-Rio
  • Vaston Costa UFCAT


This paper describes a quantum algorithm for proof search in sequent calculus of a subset of Linear Logic using the Grover Search Algorithm. We briefly overview the Grover Search Algorithm and Linear Logic, show the detailed steps of the algorithm and then present the results obtained on quantum simulators.


Alsing, P. M. and McDonald, N. (2011). Grover’s search algorithm with an entangled database state. In Quantum Information and Computation IX, volume 8057, page 80570R. International Society for Optics and Photonics.

Di Cosmo, R. and Miller, D. (2019). Linear Logic. In Zalta, E. N., editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2019 edition.

Grover, L. K. (1997). Quantum mechanics helps in searching for a needle in a haystack. Physical review letters, 79(2):325.

Piro, F., Askarpour, M., and Di Nitto, E. (2020). Generalizing an exactly-1 sat solver for arbitrary numbers of variables, clauses, and k. In 1st International Workshop on Software Engineering and Technology, Q-SET 2020, volume 2705, pages 27–37. CEUR-WS.
Como Citar

Selecione um Formato
SARAIVA, Lorenzo; HAEUSLER, Edward Hermann; COSTA, Vaston. Quantum Algorithm for Multiplicative Linear Logic. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 4. , 2023, João Pessoa/PB. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2023 . p. 33-40. ISSN 2763-8731. DOI: https://doi.org/10.5753/wbl.2023.229335.