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

DOI: https://doi.org/10.5753/wbl.2023.230566

Abstract

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.

References

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.