On the Coverage Property of a Derivation Compression Algorithm
Resumo
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.
Referências
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.
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.
Publicado
06/08/2023
Como Citar
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.
