Ցոյց տուր կառուցուածքը

Հրապարակման մանրամասներ:

"ՀՀ ԳԱԱ Զեկույցներ" հանդեսը հիմնադրվել է 1944թ.: Լույս է տեսնում տարին 4 անգամ:

Ամսագրի կամ հրապարակման վերնագիր:

ՀՀ ԳԱԱ Զեկույցներ = Доклады НАН РА = Reports NAS RA

Հրապարակման ամսաթիւ:

2013

Հատոր:

113

Համար:

1

ISSN:

0321-1339

Պաշտոնական URL:


Լրացուցիչ տեղեկութիւն:

կապին հետեւելուն համար սեղմէ հոս

Վերնագիր:

Some Generalization of Proof System “Resolution over Linear Equations”

Այլ վերնագիր:

«Գծային հավասարումների ռեզոլյուցիա» արտածումների համակարգի որոշ ընդհանրացում / Արմինե Ա. Չուբարյան, Ա. Ս. Ճիտոյան։ Некоторое обобщение системы доказательств “Резолюции над линейными равенствами” / Армине А. Чубарян, А. С. Читоян.

Ստեղծողը:

Armine A. Chubaryan ; A. S. Tchitoyan

Աջակից(ներ):

Պատ․ խմբ.՝ Վ. Հ․ Համբարձումյան (1944-1959) ; Մ․ Մ․ Ջրբաշյան (1960-1965) ; Ա․ Գ․ Նազարով (1966-1983) ; Պատ․ խմբ․ տեղակալ՝ Վ․ Հ․ Ղազարյան (1983-1986) ; Պատ․ խմբ․՝ Դ․ Մ․ Սեդրակյան (1987-1999) ; Գլխավոր խմբ․՝ Ս․ Ա․ Համբարձումյան (2000-2004) ; Վ․ Ս․ Զաքարյան (2005-2018) ; Ռ․ Մ․ Մարտիրոսյան (2018-)

Խորագիր:

Mathematics ; Science

Չվերահսկուող բանալի բառեր:

resolution systems ; resolution over linear equations ; refutation ; proof complexity ; hard provable formula.

Ծածկոյթ:

7-12

Ամփոփում:

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) правила переименования позволяет выводить те же тавтологии с полиномиальной сложностью.

Հրատարակութեան վայրը:

Երևան

Հրատարակիչ:

ՀՀ ԳԱԱ հրատ.

Ստեղծման ամսաթիւը:

2013-03-20

Տեսակ:

Հոդված

Ձեւաչափ:

pdf

Դասիչ:

АЖ 144

Թուայնացում:

ՀՀ ԳԱԱ Հիմնարար գիտական գրադարան

Բնօրինակին գտնուելու վայրը:

ՀՀ ԳԱԱ Հիմնարար գիտական գրադարան