ՀՀ ԳԱԱ Զեկույցներ =Reports NAS RA

Some Generalization of Proof System “Resolution over Linear Equations”

Chubaryan, Armine A. and Tchitoyan, A. S. (2013) Some Generalization of Proof System “Resolution over Linear Equations”. ՀՀ ԳԱԱ Զեկույցներ, 113 (1). pp. 7-12. ISSN 0321-1339

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
244Kb

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

Item Type:Article
Additional Information:«Գծային հավասարումների ռեզոլյուցիա» արտածումների համակարգի որոշ ընդհանրացում / Արմինե Ա. Չուբարյան, Ա. Ս. Ճիտոյան։ Некоторое обобщение системы доказательств “Резолюции над линейными равенствами” / Армине А. Чубарян, А. С. Читоян.
Uncontrolled Keywords:resolution systems, resolution over linear equations, refutation, proof complexity, hard provable formula.
Subjects:Q Science > QA Mathematics
ID Code:6099
Deposited By:NAS Reports
Deposited On:13 Jun 2013 15:23
Last Modified:13 Mar 2014 08:16

Repository Staff Only: item control page