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 \L{}ukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for \L{}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 \L{}ukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued \L{}ukasiewicz logics.

翻译：本文提出了Bonet和Buss针对Frege系统的证明模拟程序在演绎定理不成立逻辑中的推广。具体而言，我们研究了有限值Łukasiewicz逻辑的情形。为此，我们构建了证明系统，分别在Avron针对Łukasiewicz三值逻辑的Frege系统中引入嵌套版本和一般版本的析取消去规则。针对这些系统，我们从证明步数和证明长度两方面给出了加速的上界。我们还考虑了Tamminga的自然演绎系统和Avron针对三值Łukasiewicz逻辑的超序贯演算，并将关于析取消去规则的结果推广到所有有限值Łukasiewicz逻辑中。