Showing cs.LOShow all
2 papers · 1 filter
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.LO2025
On the horizontal compression of dag-derivations in minimal purely implicational logic
Edward Hermann Haeusler, José Flávio Cavalcante Barros Junior, Robinson
This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic . Introduce the horizontal collapsing set of rules and the algor…