Օբյեկտ

Վերնագիր: Some Generalization of Proof System “Resolution over Linear Equations”

Ստեղծողը:

Armine A. Chubaryan ; A. S. Tchitoyan

Տեսակ:

Հոդված

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

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

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

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

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

2013

Հատոր:

113

Համար:

1

ISSN:

0321-1339

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


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

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

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

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

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

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

Ծածկույթ:

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

Նույնացուցիչ:

oai:arar.sci.am:46562

Դասիչ:

АЖ 144

Թվայնացում:

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

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

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

Օբյեկտի հավաքածուներ:

Վերջին անգամ ձևափոխված:

Oct 11, 2024

Մեր գրադարանում է սկսած:

Mar 5, 2020

Օբյեկտի բովանդակության հարվածների քանակ:

24

Օբյեկտի բոլոր հասանելի տարբերակները:

https://arar.sci.am/publication/51908

Ցույց տուր նկարագրությունը RDF ձևաչափով:

RDF

Ցույց տուր նկարագրությունը OAI-PMH ձևաչափով։

OAI-PMH

Հրատարակության անուն Ամսաթիվ
Some Generalization of Proof System “Resolution over Linear Equations” Oct 11, 2024

Օբյեկտի տեսակ՝

Նման

Այս էջը օգտագործում է 'cookie-ներ'։ Ավելի տեղեկատվություն