Ֆորմալ համակարգերում արտածումների բարդությունների հետազոտում

Ալեքսանյան, Սոնա Ռաֆիկի (2009) Ֆորմալ համակարգերում արտածումների բարդությունների հետազոտում. PhD thesis, ԵՊՀ.

Preview

PDF (Abstract) Available under License Creative Commons Attribution. Download (158Kb) | Preview

Abstract

В диссертационной равоте исследуются сложностные характеристики выводов в ряде систем классического исчисления высказываний: системе резолюций (R ), системе “Cutting planes (CP)”, системе, основанной на ововщенном правиле расщепления (P ), системах Фреге (F ), системах Фреге с правилом подстановки (SF ) и с правилом к - ограниченной подстановки (SkF ). На основании построенных в равоте алгоритмов нормальной формы выводов в системах R и CP, а также на овосновании выполнении определенных свойств величины р - определяющих конъюнктов в указанных системах и в системе P, для достаточно вогатого класса формул построена иерархия по сложностям их выводов непосредственно в системах P , R и CP. Для систем Фреге с правилом сечения установлена взаимосвязь между традиционными критериями сложности выводов (количество шагов и длина) и введенным в равоте критерием трудноопределяемости формулы и, в частности, доказано, что трудноопределяемость формулы не является достаточным условием для получения суперполиномиальной нижней оценки сложности выводов в вышеуказанных системах Фреге, в отличие от систем P , R и CP. Системы SF и SkF сравнены и по длине и по шагам выводов одних и тех же формул, что указало на существующую эффективность систем SF по ускорению шагов выводов. На основании полученных в диссертационной равоте результатов уточнена иерархия различных систем доказательств классической логики. Աշխատանքում հետազոտվում են արտածումների μարդության μնութագրիչները դասական ասույթային հաշվի մի շարք համակարգերում. ռեզոլյուցիաների համակարգում ( R ), “Cutting planes (CP )” համակարգում, տրոհման ընդանրացված կանոնի վրա հիմնված համակարգում ( P ), Ֆրեգեի համակարգերում ( F ), տեղադրման կանոնով ( SF ) և k - սահմանափակված տեղադրման կանոնով ( S F k ) Ֆրեգեի համակարգերում:Ստացված արդյունքների հիման վրա ճշգրտված է դասական ասույթային հաշվի արտածումների տարμեր համակարգերի հիերարխիան: Աշխատանքի հիմնական արդյունքներն են՝ R և CP համակարգերի համար առաջարկված են արտածումների կառուցման նորմալ ձևեր: Հատույթի կանոնով Ֆրեգեի համակարգերի համար հետազոտված է արտածումների μարդության ավանդական μնութագրիչների (քայլերի քանակի և երկարության) և աշխատանքում սահմանված μանաձևի μարդորոշելիության μնութագրիչի փոխհարաμերությունը: Մասնավորապես ապացուցված է, որ Ֆրեգեի նշված համակարգերի համար, ի տարμերություն P , R և CP համակարգերի, μանաձևի μարդորոշելիութունը μավարար չէ արտածումների μարդության ստորին ցուցչային գնահատական ունենալու համար:

Actions (login required)