On the Coverage Property of a Derivation Compression Algorithm - B. Filho, Robinson C. de M.; Santos, Jefferson de B.; Haeusler, Edward Hermann (Anais do Workshop Brasileiro de Lógica (WBL), 2023)
We further elaborate, with a short example, on the set of compression rules and the derivation compression algorithm presented in [Haeusler et al. 2023]. We also argue a proof, done with the Lean theorem prover, that this algorithm obtains a dag-like compressed derivation from any tree-like Natural Deduction derivation in Minimal Purely Implicational Logic.