Publication Details:
"ՀՀ ԳԱԱ Զեկույցներ" հանդեսը հիմնադրվել է 1944թ.: Լույս է տեսնում տարին 4 անգամ:
Journal or Publication Title:
ՀՀ ԳԱԱ Զեկույցներ = Доклады НАН РА = Reports NAS RA
Date of publication:
Volume:
Number:
ISSN:
Official URL:
Additional Information:
Title:
Some Generalization of Proof System “Resolution over Linear Equations”
Other title:
Creator:
Armine A. Chubaryan ; A. S. Tchitoyan
Contributor(s):
Պատ․ խմբ.՝ Վ. Հ․ Համբարձումյան (1944-1959) ; Մ․ Մ․ Ջրբաշյան (1960-1965) ; Ա․ Գ․ Նազարով (1966-1983) ; Պատ․ խմբ․ տեղակալ՝ Վ․ Հ․ Ղազարյան (1983-1986) ; Պատ․ խմբ․՝ Դ․ Մ․ Սեդրակյան (1987-1999) ; Գլխավոր խմբ․՝ Ս․ Ա․ Համբարձումյան (2000-2004) ; Վ․ Ս․ Զաքարյան (2005-2018) ; Ռ․ Մ․ Մարտիրոսյան (2018-)
Subject:
Uncontrolled Keywords:
resolution systems ; resolution over linear equations ; refutation ; proof complexity ; hard provable formula.
Coverage:
Abstract:
It is known that many tautologies, which require the exponential lower bounds of proof complexities in resolution system (R), have polinomially bounded proofs in the system R(lin) - “Resolution over linear equations”. Sequence of tautologies, which require the exponential lower bounds of proof complexities in R(lin) are shown. After adding the renaming rule, mentioned collections have polynomially bounded proof complexity. Հայտնի է, որ բազմաթիվ նույնաբանություններ, որոնք արտածվում են R՝ ռեզոլյուցիոն համակարգում ոչ պակաս, քան ցուցչային բարդությամբ, R(lin)՝ «Գծային հավասարումների ռեզոլյուցիա» համակարգում արտածվում են բազմանդամային բարդությամբ: Աշխատանքում ցույց է տրվում, որ գոյություն ունի նույնաբանությունների այնպիսի հաջորդականություն, որոնց արտածման բարդությունները R(lin)-ում ունեն ստորին ցուցչային գնահատական: Վերանվանման կանոնի ավելացումը R(lin)-ին թույլ է տալիս նշված նույնաբանությունները արտածել բազմանդամային ժամանակում: Известно, что многие тавтологии, выводимые в системе резолюций (R) с не менее чем экспоненциальной сложностью, в системе “Резолюции над линейными равенствами” (R(lin)) выводятся с полиномиальной сложностью. Доказывается, 1 2 что существует последовательность тавтологий, которые выводятся в системе R(lin) с не менее чем экспоненциальной сложностью. Добавление к системе R(lin) правила переименования позволяет выводить те же тавтологии с полиномиальной сложностью.
Place of publishing:
Երևան
Publisher:
Date created:
Type:
Format:
Call number:
Digitization:
ՀՀ ԳԱԱ Հիմնարար գիտական գրադարան