On the Coverage Property of a Derivation Compression Algorithm

  • Robinson C. de M. B. Filho PUC-Rio
  • Jefferson de B. Santos FGV
  • Edward Hermann Haeusler PUC-Rio


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.


Barros Júnior, J. and Haeusler, E. (2019). A comparative study on compression techniques for Propositional Proofs. In Book of Abstracts, 19th Braz. Meeting on Logic, pages 85–86, Brazil.

de Moura, L., Kong, S., and Avigad, J. (2023). Theorem Proving in Lean.

Haeusler, E., Moura Brasil Filho, R., and Barros Júnior, J. (2023). On the horizontal compression of dag-derivations in minimal purely implicational logic.

Prawitz, D. (1965). Natural Deduction: Proof-Theoretical Study. Dover Publications.
Como Citar

Selecione um Formato
B. FILHO, Robinson C. de M.; SANTOS, Jefferson de B.; HAEUSLER, Edward Hermann. On the Coverage Property of a Derivation Compression Algorithm. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 4. , 2023, João Pessoa/PB. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2023 . p. 1-8. ISSN 2763-8731. DOI: https://doi.org/10.5753/wbl.2023.230566.