Հայաստանի ատենախոսությունների բաց մատչելիության պահոց = Open Access Repository of the Armenian Electronic Theses and Dissertations (Armenian ETD-OA) = Репозиторий диссертаций Армении открытого доступа

«Բարդ որոշելի» բանաձևերի արտածումների բարդությունները ասույթային հաշվի համակարգերում

Աբաջյան, Աշոտ Գասպարի (2012) «Բարդ որոշելի» բանաձևերի արտածումների բարդությունները ասույթային հաշվի համակարգերում. PhD thesis, ԵՊՀ.

[img]
Preview
PDF (Abstract)
Available under License Creative Commons Attribution.

Download (226Kb) | Preview

    Abstract

    Ատենախոսությունում հետազոտված են որոշ դասերի բանաձևերի արտածումների բարդության բնութագրիչները դասական ասույթային հաշվի մի շարք համակարգերում: Ի լրումն նախկինում հայտնի «բարդ որոշելի» բանաձևերի գաղափարին` սույն աշխատանքում ներմուծվել է «քվազի բարդ որոշելի» բանաձևի գաղափարը: Բարդ որոշելի և քվազի բարդ որոշելի մի շարք բանաձևերի դասերի համար հետազոտվել են արտածումների քայլերի քանակները և երկարությունները դասական ասույթային հաշվի կոնյունկտիվ նորմալ ձևերի կամ դիզյունկտիվ նորմալ ձևերի վրա հիմնված մի քանի հայտնի համակարգերում` տրոհման ծառերում (ST), ռեզոլյուցիայի համակարգում (R), գծային ռեզոլյուցիայի համակարգում (R(lin) ), Գալիերի կողմից ներմուծված GCNF՛ համակարգում և Նորիկո Արայիի կողմից ներմուծված GCNF՛+տեղափոխություն համակարգում, որոնցից վերջին երեքը քիչ են ուսումնասիրված: Բարդ որոշելի և քվազի բարդ որոշելի բանաձևերի սահմանումը հիմնված է որոշիչ կոնյունկտի և որոշիչ դիզյունկտիվ նորմալ ձևի գաղափարների վրա, ինչը թույլ է տալիս ուսումնասիրված դասերի բանաձևերի համար վերոհիշյալ համակարգերում համեմատաբար դյուրին եղանակով ստանալ արտածումների բարդության բնութագրիչների ստորին գնահատականները, և հիմնական ուշադրությունը դարձվել է նույն կարգի վերին գնահատականներ ստանալու խնդիրներին: В диссертации исследованы сложностные характеристики выводов некоторых классов “трудноопределяемых” и “квазитрудноопределяемых” формул в ряде систем доказательств классического исчисления высказываний. В работе для любой пропозициональной формулы введены понятия определяющего конъюнкта и определяющей дизъюнктивной нормальной формы. Определяющей длиной d(ф) формулы ф называется минимальное количество переменных, придавая значения которым можно определить значение ф (0 или 1) вне зависимости от значений остальных переменных формулы ф. Если для последовательности формул фф длины фф и ^ (фп) одинаковы по порядку, то такие формулы называются трудноопределяемыми, если же d (фп) растет с ростом длины ф , то такие формулы–квазитрудноопределяемые. В диссертации исследованы количество шагов и длины выводов одного класса квази-трудноопределяемых формул (Т^п) и некоторого класса трудноопределяемых формул (ТТМ ) в ряде опровергающих систем Н,2п ֊1 доказательств (дереве расщеплений (57), резолюций (К), резолюций над линейными равенствами (Я(1ш)) и системе ОСЫЯ+регти1:а1:юп). Диссертационная работа состоит из введения и трех глав. Во введении даны краткая характеристика диссертации и обзор результатов, на базе которых проведены исследования диссертации и некоторые общеизвестные определения. In this thesis the proof complexity characteristics of some classes of hard determinable and quasi-hard determinable formulas are investigated in different proof systems of Classical Propositional Logic. For every propositional formula the notions of determinative conjunct and determinative disjunctive normal form are introduced. The determinative length d (p) of formula p is denoted as the minimal number of variables, some values of which can produce the value of p (0 or 1) independently of the values of the remaining variables in p. The formulas p are called hard determinable if the length of p and d (pn) are equal by order. The formulas p are called quasi-hard determinable if d (pn) increase with the increase of the length of p. In this thesis the number of steps and sizes of proofs are investigated for some class of quasi-hard determinable formulas (Tsgfn) and some class of hard determinable formulas (TTM ) in different refutation proof systems (Split Tree (ST), Resolution n,2n-1 (R), Resolution over linear equations (R(llnJ) and GCNF+permutation). The thesis consists of Introduction and three parts. The main characteristics of the thesis, the known results, on the base of which the results of our investigation are obtained, and some well-known definitions are given in Introduction.

    Item Type: Thesis (PhD)
    Additional Information: Сложности выводов трудноопределяемых формул в системах исчисления высказываний.
    Uncontrolled Keywords: Абаджян Ашот Гаспарович, Abajyan A.A.
    Subjects: Mathematics and Cybernetics
    Divisions: UNSPECIFIED
    Depositing User: NLA Circ. Dpt.
    Date Deposited: 27 Nov 2015 10:30
    Last Modified: 13 Mar 2017 13:12
    URI: http://etd.asj-oa.am/id/eprint/42

    Actions (login required)

    View Item