|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Bussстатья
Информация о цитировании статьи получена из
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 26 июня 2019 г.
- Автор: Kozhemiachenko Daniil
- Журнал: Journal of Applied Non-classical logics
- Том: 28
- Номер: 4
- Год издания: 2018
- Первая страница: 389
- Последняя страница: 413
- DOI: 10.1080/11663081.2018.1525208
- Аннотация: 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\vee}}$ and $\L_{3_\vee}$ which augment Avron's Frege system H\L{}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 G\L{}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.
- Добавил в систему: Кожемяченко Даниил Андреевич