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…