Object structure

Publication Details:

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

Journal or Publication Title:

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

Date of publication:

2013

Volume:

113

Number:

1

ISSN:

0321-1339

Official URL:


Additional Information:

click here to follow the link

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:

Mathematics ; Science

Uncontrolled Keywords:

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

Coverage:

7-12

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:

2013-03-20

Type:

Հոդված

Format:

pdf

Call number:

АЖ 144

Digitization:

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

Location of original object:

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