Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Bussстатья

Информация о цитировании статьи получена из Scopus
Дата последнего поиска статьи во внешних источниках: 26 июня 2019 г.

Работа с статьей


[1] Kozhemiachenko D. Generalisation of proof simulation procedures for frege systems by m.l. bonet and s.r. buss // Journal of Applied Non-classical logics. — 2018. — Vol. 28, no. 4. — P. 389–413. 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 L_{3_{n∨}} and L_{3_∨} which augment Avron's Frege system HL{}uk 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 GL{}uk for 3-valued L{}ukasiewicz logic L_3 and generalise our results considering the disjunction elimination rule to all finite-valued L{}ukasiewicz logics. [ DOI ]

Публикация в формате сохранить в файл сохранить в файл сохранить в файл сохранить в файл сохранить в файл сохранить в файл скрыть