2 papers
cs.LO2026
From Dag-Like Proofs to Boolean Circuits in Lean
Lorenzo Saraiva, Edward Hermann Haeusler
In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational m…
cs.LO2023
Quantum Algorithm for Multiplicative Linear Logic
Lorenzo Saraiva, Edward Hermann Haeusler, Vaston Costa
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 A…