Journal or Publication Title:
Date of publication:
Volume:
ISSN:
Official URL:
Additional Information:
Թամազյան Հակոբ Ա., Չուբարյան Անահիտ Ա., Tamazyan Hakob A., Chubaryan Anahit A.
Title:
Об отношениях сложностей выводов в ряде систем исчисления высказываний
Other title:
Ասույթային հաշվի մի շարք համակարգերում արտածումների բարդության հարաբերությունների մասին ; On Proof Complexities Relations in Some Systems of Propositional Calculus
Creator:
Тамазян, Акоп A. ; Чубарян, Анаит А.
Subject:
Uncontrolled Keywords:
разновидности секвенциальных систем исчислениявысказываний ; разновидности систем Фреге ; количество щагов вывода ; экспоненциальное ускорение
Coverage:
Abstract:
Для некоторых семейств формул сравнены количествa шагов линейных выводов в ряде систем исчисления высказываний: секвенциальной системе с правилом сечения PK, в той же системе без правила сечения PK—, в той же системе с добавлением правила подстановки SPK, в той же системе с добавлением кванторов QPK. Для одного из рассмотренных семейств формул Алессандрой Карбоне в [1] сравнены количествa шагов выводов в виде дерева в тех же системах исчисления высказываний и выявлено отличительное свойство системы QPK, а именно доказано экспоненциальное ускорение по отношению к системам SPK и PK, которые,, в свою очередь,, имеют экспоненциальное ускорение по отношению к системе PK—. Этот результат послужил толчком для бурного интереса к исследованиям системы QPK. В настоящей работе для линейных выводов получены иные сотношения количествa шагов в тех же системах: оказалось, что система QPK не имеет преимуществ по отношению к системе SPK, оказалось также, что для рассматриваемых семейств формул система PK не имеет преимуществ по отношению к системе PK—, которая, в свою очередь, не имеет преимуществ по отношению к более слабой монотонной системе PMon. Доказана также достоверность полученных результатов для ряда иных семейств формул и ряда других систем. Բանաձևերի մի քանի ընտանիքների համար համեմատված է գծային արտածումների քայլերի քանակը ասույթային հաշվի մի քանի համակարգերում՝ հատույթի կանոնով սեկվենցիալ համակարգում – PK, առանց հատույթի կանոնի նույն համակարգում - PK—, տեղադրման կանոնով նույն համակարգում - SPK, ծավալիչների ավելացմամբ նույն համակարգում - QPK. Մեր կողմից դիտարկված բանաձևերի մեկ ընտանիքի համար Ալեսսանդրա Կարբոնեի կողմից [1]-ում համեմատված են ծառատիպ արտածումների քայլերի քանակը հիշատակված համակարգերում և հայտնաբերված է QPK համակարգի գերակայությունը՝ ապացուցված է, որ այն ունի էքսպոնենցիալ արագացում SPK և PK համակարգերի նկատմամբ, իսկ վերջինները, իրենց հերթին, ունեն էքսպոնենցիալ արագացում PK— համակարգի նկատմամբ: Այս արդյունքը առիթ հանդիսացավ QPK համակարգի հանդեպ հետազոտումների բուռն հետաքրքրությունների համար: Սույն աշխատությունում այդ նույն համակարգերի համար ստացվել են գծային արտածումների քայլերի բոլորովին այլ հարաբերություններ՝ պարզվել է, որ QPK համակարգը չունի որևէ առավելություն SPK համակարգի նկատմամբ, պարզվել է նաև, որ բանաձևերի դիտարկվող ընտանիքների համար PK համակարգը ևս չունի առավելություն PK— համակարգի նկատմամբ, որն իր հերթին չունի որևէ առավելություն առավել թույլ, մոնոտոն PMon համակարգի նկատմամբ: Ապացուցված է նաև ստացված արդյունքների իսկությունը բանաձևերի այլ ընտանիքների, ինչպես նաև այլ համակարգերի համար: The number of linear proofs steps for some sets of formulas is compared in the folowing systems of propositional calculus: PK – seguent system with cut rule, PK— - the same system without cut rule, SPK – the same system with substitution rule, QPK – the same system with quantifier rules. The number of steps of tree-like proofs in the same systems for some considered set of formulas is compared from Alessandra Carbone in [1] and some distinctive property of the system QPK is revealed: QPK has an exponential speed-up over the systems SPK and PK, which, in their turn, have an exponential speed-up over the system PK—. This result drew the heavy interest for the study of the system QPK. In this work for linear proofs steps in the same systems the other relations are received: it is showed that the system QPK has no preference over the system SPK, it is showed also that for the considered formula sets the system PK has no preference over the system PK—, which, in its turn, has no preference over the monotone system PMon. It is proved also, that the same results are reliable for some other sets of formulas and for other systems as well.