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

SLDNF-ռեզոլյուցիայի մասին ժխտումով տրամաբանական ծրագրավորման մեջ

Սարգսյան, Լուսինե Արամայիսի (2012) SLDNF-ռեզոլյուցիայի մասին ժխտումով տրամաբանական ծրագրավորման մեջ. PhD thesis, ԵՊՀ.

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

Download (503Kb) | Preview

    Abstract

    Диссертационная работа посвящена проблемам логического программирования. Объектами исследования являются логические программы и запросы, использующие отрицание. Предпринимается попытка распространить методы логического программирования на формулы более сложного вида, нежели хорновские дизъюнкты, для того, чтобы увеличить выразительные возможности логических программ. На самом деле невозможно выразить негативные знания посредством хорновских дизъюнктов, а программа в логическом программировании по определению состоит из хорновских дизъюнктов, пригодных для представления только позитивной информации. Для представления и получения негативной информации необходимо ввести специальные правила, руководствуясь принципами, важнейшими из которых являются допущение замкнутости мира (Closed World Assumption) и отрицание по неуспеху (Negation as Failure). В реальных системах логического программирования программы могут содержать отрицание в телах своих правил, отрицание могут содержать также и запросы. И конечно, системы логического программирования должны быть снабжены механизмом обработки отрицательных подцелей. Метод, который обычно выбирается при таких случаях, это расширение SLD-резолюции, основываясь на принципе отрицания по неуспеху (NF), при использовании которого отрицательная цель характеризуется неудачей или успехом соответствующей цели без отрицания. Расширенная таким образом резолюция называется SLDNF-резолюцией1. Семантика отрицания по неуспеху не совпадает с семантикой логического отрицания: нельзя считать что-то неверным, потому что оно является недоказуемым. Чтобы дать теоретическое обоснование корректности SLDNF-резолюции и совместить логические и процедурные отрицания, вводится понятие замыкания программы. Основная идея состоит в том, чтобы рассматривать предикаты, описанные в некоторой программе P как полностью определенные. Т. е. программе P сопоставляется формула логики предикатов первого порядка с равенством comp(P) таким образом, чтобы логическая семантика соответствовала допущению замкнутости мира1,2. Ատենախոսությունը նվիրված է տրամաբանական ծրագրավորման պրոբլեմներին: Հետազոտվում են ընդհանրացված տրամաբանական ծրագրեր և հարցումներ (տրամաբանական ծրագրեր և հարցումներ, որոնցում կարող է ժխտում օգտագործվել): Հորնի ծրագրավորման դեպքում տրամաբանական ծրագիրը բաղկացած է միայն դրական ինֆորմացիա ներկայացնելու համար պիտանի Հորնի դիգյունկտներից: Բացասական ինֆորմացիա ներկայացնելու համար անհրաժեշտ է ընդլայնել ծրագրի սահմանումը թույլատրելով ժխտման օգտագործում ծրագրի կանոնների մարմիններում: Պարզ է, որ տրամաբանական ծրագրավորման համակարգերն այդ դեպքում պետք է օժտված լինեն բացասական ինֆորմացիան մշակելու մեխանիզմներով: Նման դեպքերում սովորաբար կիրառվում է ժխտումը որպես ձախողում (Negation as Failure) կանոնով ընդլայնված ՏՀՕ-ռեզոլ|ուցիան' SLDNF- ռեզորուցիան: Հիմնավորելու համար ժխտումը որպես ձախողում կանոնի օգտագործումը Կ.Քլարկի կողմից առաջարկվեց ծրագրի «փակման» հասկացությունը, որի առանցքային գաղափարը ծրագրում օգտագործվող բոլոր պրեդիկատներն ամբողջությամբ սահմանված համարելն է: Այսինքն, P ընդհանրացված ծրագրին համապատասխանեցվում է առաջին կարգի պրեդիկատների տրամաբանության comp(P) բանաձև (որն օգտագործում է հավասարություն) համաձայն փակ աշխարհի ենթադրության: Ապացուցված է SLDA^F-ռեզոլ^ուցիայի անհակասելիությունն այն իմաստով, որ եթե P ընդհանրացված ծրագրի և Q ընդհանրացված հարցման համար (P,Q) զույգից SLDNF-ռեզոլյուցիայի միջոցով արտածվում է դատարկ հարցում, ապա comp(P) բանաձևից տրամաբանորեն բխում է Q հարցումը, իսկ եթե (P,Q) զույգի համար կառուցվում է ձախողման վերջավոր SLDNF-ծառ, ապա comp(P) բանաձևից տրամաբանորեն բխում է Q հարցման ժխտումը: Հայտնի է, որ ընդհանուր դեպքում SLDAF-ռեզոլյուցիան լրիվ չէ, այսինքն հնարավոր է, որ comp(P) բանաձևից տրամաբանորեն բխի հարցումը կամ նրա ժխտումը, սակայն SLDAF-ռեզոլյուցիայի միջոցով պատասխան ստանալ հնարավոր չլինի: Ուստի հետաքրքրություն է ներկայացնում SZDAF-ռեզորուցիայի լրիվության ուսումնասիրությունը ծրագրերի և հարցումների ենթադասերում: The thesis is devoted to problems of logic programming. General logic programs (logic programs with negation) and general goals (goals with negation) are investigated. A logic program in Horn programming consists of Horn disjuncts, which are useful only to represent positive information. In order to represent negative information, it is important to extend the definition of programs to include negative literals in the bodies of clauses. Logic programming systems also require a mechanism for handling negative information. The method usually chosen is SLZNFresolution, which is the extension of SLZ-resolution with the negation as failure rule. In order to justify the use of the negation as failure rule Clark introduced the concept of the completion of a general program, the key idea of which is to treat all predicates of a program as fully defined. More precisely a formula comp(P) of the first- order logic (with equality) is associated with a program P in accordance with the closed world assumption. It is known that SLZNFresolution is sound in the sense that if for a general program Pand a general goal Q there exists a derivation of the empty goal from (P,Q), then Q is a logical consequence of comp(P), and if there exists a finitely failed SLDNF-tree for (P,Q), then the negation of Q is a logical consequence of comp(P). It is also known that in general SLZNFresolution is not complete, i.e. a goal Qor its negation can be a logical consequence of comp(P), but it is not possible to get a response for (P,Q) via SLZNFresolution. Naturally the question arises about the completeness of SLZNFresolution in some subclasses of the programs and goals. Practical logic programming systems use built-in predicates, that are implemented differently to those defined by Horn disjuncts. Moreover, some built-in predicates cannot be represented by pure Horn disjuncts. The modification of SLZ-resolution for Horn programming with built-in predicates is introduced by S.Vigiyan and its completeness and soundness has been established. However, practical logic programming systems use both negation and built-in predicates, and a modification of SLZNF-resolution for built-in predicates is required. The objectives of this thesis are to investigate the completeness of SLZNF-resolution in some subclasses of general programs and goals, to introduce a modification of SLZNF- resolution for built-in predicates and investigate the soundness of the modified SLZNF- resolution, as well as to study SLZNF-resolution rules used in practical systems (the domain of definition of such rules is a subset of the domain of definition of SLZNF-resolution rules), and investigate their soundness.

    Item Type: Thesis (PhD)
    Additional Information: SLDNF-ռեզոլյուցիայի մասին ժխտումով տրամաբանական ծրագրավորման մեջ: On SLDNF-resolution in logic programming with negation.
    Uncontrolled Keywords: Սարգսյան Լուսինե Արամայիսի, Sargsyan Lusine A.
    Subjects: Mathematics and Cybernetics
    Divisions: UNSPECIFIED
    Depositing User: NLA Circ. Dpt.
    Date Deposited: 10 Mar 2017 15:09
    Last Modified: 13 Mar 2017 09:41
    URI: http://etd.asj-oa.am/id/eprint/4260

    Actions (login required)

    View Item