کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4661558 1633434 2017 41 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Proof complexity of intuitionistic implicational formulas
ترجمه فارسی عنوان
پیچیدگی اثبات فرمول استلزام شهودی
کلمات کلیدی
پیچیدگی اثبات؛ منطق شهودی؛ قطعه استلزام
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions.In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubeš (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jeřábek (2009), can be realized by implicational tautologies.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 168, Issue 1, January 2017, Pages 150–190
نویسندگان
,