Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917613933690880 |
|---|---|
| author | Kozhemiachenko, Daniil |
| author_facet | Kozhemiachenko, Daniil |
| contents | In this paper, we present a~generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for Łukasiewicz three-valued logic with nested and general versions of the disjunction elimination rule, respectively. For these systems we provide upper bounds on speed-ups w.r.t.\ both the number of steps in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_09119 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss Kozhemiachenko, Daniil Logic Logic in Computer Science In this paper, we present a~generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for Łukasiewicz three-valued logic with nested and general versions of the disjunction elimination rule, respectively. For these systems we provide upper bounds on speed-ups w.r.t.\ both the number of steps in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. |
| title | Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2403.09119 |