Power Point

Report
‫استنتاج در منطق مرتبه اول‬
‫تهيه کننده‪ :‬عبدالرضا ميرزايي‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫سرفصل مطالب‬
‫تقليل استنتاج مرتبه‪-‬اول به استنتاج گزاره اي‬
‫يكسان سازي )‪(Unification‬‬
‫‪ MP‬تعميم يافته )‪(GMP‬‬
‫زنجيره استنتاج روبه جلو‬
‫زنجيره استنتاج رو به عقب‬
‫رزولوشن‬
‫‪2‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
Universal instantiation
‫نمونه سازي عمومي‬
‫ توسط آن جمله‬،‫• هر نمونه از يك جمله داراي سور عمومي‬
.‫قابل استلزام است‬
‫• مثال‬
• x King(x)  Greedy(x)  Evil(x) :
King(John)  Greedy(John)  Evil(John)
King(Richard)  Greedy(Richard)  Evil(Richard)
King(Father(John))  Greedy(Father(John))  Evil(Father(John))
.
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
3
‫نمونه سازي وجودي‬
‫‪Existential instantiation‬‬
‫• مثال‬
‫‪• x Crown(x)  OnHead(x,John) :‬‬
‫)‪Crown(C1)  OnHead(C1,John‬‬
‫• که ‪ C1‬يك سمبول جديد مي باشد‪ ،‬كه به آن ثابت ‪ Skolem‬گويند‬
‫‪4‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫تقليل به استنتاج گزاره اي‬
‫ فقط شامل جمالت زير باشد‬KB ‫فرض کنيد‬
x King(x)  Greedy(x)  Evil(x)
King(John)
Greedy(John)
Brother(Richard,John)
:‫ داريم‬،‫با نمونه سازي جمله داراي سور عمومي به تمام طرق ممكن‬
King(John)  Greedy(John)  Evil(John)
King(Richard)  Greedy(Richard)  Evil(Richard)
King(John)
Greedy(John)
Brother(Richard,John)
‫ سمبول‬.)‫ جديد به فرم گزاره اي درآمده است(گزاره اي سازي‬KB •
:‫هاي گزاره اي عبارتند از‬
King(John), Greedy(John), Evil(John), King(Richard), etc.
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
5
‫تقليل به استنتاج گزاره اي‬
‫•‬
‫•‬
‫•‬
‫•‬
‫هر پايگاه دانش در ‪ FOL‬مي تواند به گونه اي گزاره اي‬
‫سازي شود كه ايجاب را حفظ كند‪.‬‬
‫يک ‪ ground sentence‬توسط ‪ KB‬جديد قابل ايجاب است‬
‫اگر و فقط اگر توسط ‪ KB‬اصلي قابل ايجاب باشد‬
‫ايده‪ KB :‬و ‪ query‬را گزاره اي سازي كن‪ ،‬رزولوشن را‬
‫اعمال و نتيجه را برگردان‬
‫مشكل‪ :‬در مورد سمبول هاي تابعي تعداد نامحدودي‬
‫‪ ground term‬وجود دارد‪ ،‬مثالا‪:‬‬
‫)))‪Father(Father(Father(John‬‬
‫‪6‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫تقليل به استنتاج گزاره اي‬
‫• قضيه )‪ :Herbrand (1930‬اگر جمله ي ‪ α‬توسط يک ‪ FOL KB‬قابل‬
‫ايجاب باشد آنگاه اين جمله توسط زيرمجموعه محدودي از پايگاه‬
‫دانش گزاره اي سازي شده قابل ايجاب است‪.‬‬
‫‪For n = 0 to ∞ do‬‬
‫‪create a propositional KB by instantiating with depth-n terms‬‬
‫‪see if α is entailed by this KB‬‬
‫• مشکل‪ :‬اگر‪ KB‬جمله ‪ α‬را ايجاب کند كار مي كند‪ ،‬در غير اينصورت‬
‫در حلقه بي نهايت مي افتد‪.‬‬
‫• قضيه )‪ : Turing (1936), Church (1936‬ايجاب در ‪ FOL‬نيمه‬
‫تصميم پذير است‪.‬‬
‫• الگوريتم هايي وجود دارند كه براي هر جمله قابل ايجاب پاسخ بله را توليد‬
‫مي كنند‪ ،‬ولي الگوريتمي وجود ندارد كه براي هر جمله اي كه قابل ايجاب‬
‫نباشد پاسخ خير توليد كند‪.‬‬
‫‪7‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫مشكالت گزاره اي سازي نمودن‬
‫به نظر مي رسد كه گزاره اي سازي كردن جمالت نامربوط زيادي‬
‫توليد مي كند‪ .‬براي مثال از جمالت زير‪:‬‬
‫)‪x King(x)  Greedy(x)  Evil(x‬‬
‫)‪King(John‬‬
‫)‪y Greedy(y‬‬
‫)‪Brother(Richard,John‬‬
‫بديهي است كه )‪ Evil(John‬اما گزاره اي سازي كردن حقايق زيادي‬
‫مانند )‪ Greedy(Richard‬توليد مي كند كه نامربوط مي باشند‬
‫با ‪ p‬تا ‪ predicate‬از نوع ‪ k‬تايي و ‪ n‬ثابت ‪ p·nk‬نمونه سازي وجود‬
‫دارد‪.‬‬
‫‪8‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫يكسان سازي‬
‫‪Unification‬‬
‫• اگر بتوانيم يك جانشيني مانند‪ θ‬بيابيم به گونه اي که )‪ King(x‬و‬
‫)‪ Greedy(x‬با )‪ King(John‬و )‪Greedy(y‬تطبيق يابند‪ ،‬آنگاه نتيجه‬
‫استنتاج بالفاصله بدست مي آيد‪.‬‬
‫‪θ‬‬
‫}‪{x/Jane‬‬
‫}‪{x/OJ,y/John‬‬
‫})‪{y/John,x/Mother(John‬‬
‫}‪{fail‬‬
‫‪Unify(α,β) = θ if αθ = βθ‬‬
‫‪p‬‬
‫‪q‬‬
‫)‪Knows(John,x) Knows(John,Jane‬‬
‫)‪Knows(John,x) Knows(y,OJ‬‬
‫))‪Knows(John,x) Knows(y,Mother(y‬‬
‫)‪Knows(John,x) Knows(x,OJ‬‬
‫استاندارد سازي متغيرها از روي هم افتادن نامها جلوگيري مي کند‪ :‬مثالا‬
‫‪9‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫)‪Knows(z17,OJ‬‬
‫يكسان سازي‬
‫• براي يكسازي سازي )‪ Knows(John,x‬و )‪ Knows(y,z‬دو‬
‫جانشيني وجود دارد يا‬
‫} ‪• θ = {y/John, x/z‬‬
‫}‪• θ = {y/John, x/John, z/John‬‬
‫• اولين يكسان ساز عمومي تر از دومي مي باشد‬
‫• فقط يك عمومي ترين يكسان ساز )‪most general unifier (MGU‬‬
‫وجود دارد كه نسبت به تغيير نام متغيرها منحصر به فرد مي‬
‫باشد‪.‬‬
‫} ‪MGU = { y/John, x/z‬‬
‫‪10‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫الگوريتم يكسان سازي‬
‫‪11‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫الگوريتم يكسان سازي‬
‫‪12‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫)‪Generalized Modus Ponens (GMP‬‬
‫• ‪ GMP‬با پايگاه دانشي از ‪clause‬هاي معين (دقيقا ا يك ليترال‬
‫مثبت) كار مي كند‬
‫• فرض مي شود كه تمام متغيرها داراي سور عمومي هستند‪.‬‬
‫‪13‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫پايگاه دانش نمونه‬
• The law says that it is a crime for an American
to sell weapons to hostile nations. The country
Nono, an enemy of America, has some missiles,
and all of its missiles were sold to it by Colonel
West, who is American.
• Prove that Colonel West is a criminal
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
14
‫پايگاه دانش نمونه‬
... it is a crime for an American to sell weapons to hostile nations:
American(x)  Weapon(y)  Sells(x,y,z)  Hostile(z)  Criminal(x)
Nono … has some missiles, i.e., x Owns(Nono,x)  Missile(x):
Owns(Nono,M1) and Missile(M1)
… all of its missiles were sold to it by Colonel West
Missile(x)  Owns(Nono,x)  Sells(West,x,Nono)
Missiles are weapons:
Missile(x)  Weapon(x)
An enemy of America counts as "hostile“:
Enemy(x,America)  Hostile(x)
West, who is American …
American(West)
The country Nono, an enemy of America …
Enemy(Nono,America)
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
15
‫الگوريتم استنتاج رو به جلو‬
‫‪16‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫اثبات توسط استنتاج رو به جلو‬
‫اثبات توسط استنتاج رو به جلو‬
‫اثبات توسط استنتاج رو به جلو‬
‫خصوصيات استنتاج رو به جلو‬
‫• براي ‪first-order definite clause‬ها كامل و صحيح‬
‫است‪.‬‬
‫‪Datalog = first-order definite clauses + no functions‬‬
‫• ‪ FC‬براي ‪ Datalog‬با تعداد تكرارهاي محدودي متوقف مي‬
‫شود‪.‬‬
‫• در حالت كلي‪ ،‬اگر پايگاه دانش ‪ α‬را ايجاب نکند‪ ،‬ممكن‬
‫است متوقف نشود‪.‬‬
‫• اين امر اجتناب ناپذير است‪ :‬ايجاب با ‪Clause‬هاي معين‬
‫نيمه تصميم پذير است‬
‫‪20‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫كارآيي استنتاج رو به جلو‬
‫• استنتاج رو به جلوي افزايشي‬
‫‪Incremental forward chaining‬‬
‫• در تکرار ‪ k‬نياز به تطبيق قانوني كه هيچ كدام از شرايطش در تكرار‬
‫‪ k-1‬اضافه نشده اند‪ ،‬نيست‬
‫• خود انطباق مي تواند پرهزينه باشد‪:‬‬
‫• شاخص بندي پايگاه داده ‪ Database indexing‬اجازه مي دهد كه حقايق‬
‫شناخته شده در زمان )‪ O(1‬بازيابي شوند‪.‬‬
‫• انطباق ‪ fact‬ها در مقابل شرطهايي که به صورت ترکيب عطفي‬
‫هستند ‪ NP-hard‬است‪.‬‬
‫• استنتاج رو به جلو به طور گسترده اي در پايگاه هاي داده‬
‫استنتاجي به كار مي رود‬
‫‪21‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫مثال از انطباق سخت‬
Diff(wa,nt)  Diff(wa,sa)  Diff(nt,q) 
Diff(nt,sa)  Diff(q,nsw)  Diff(q,sa) 
Diff(nsw,v)  Diff(nsw,sa)  Diff(v,sa) 
Colorable()
Diff(Red,Blue)
Diff (Red,Green)
Diff(Green,Red) Diff(Green,Blue)
Diff(Blue,Red)
Diff(Blue,Green)
• Colorable() is inferred iff the CSP has a solution
‫الگوريتم استنتاج رو به عقب‬
‫))‪SUBST(COMPOSE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p‬‬
‫‪23‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫مثال استنتاج رو به عقب‬
‫خصوصيات استنتاج روبه عقب‬
‫• اثبات‪ :‬جستجوي اول‪-‬عمق بازگشتي – فضاي حالت بر‬
‫حسب اثبات خطي‬
‫• ناكامل به دليل وجود حلقه هاي بينهايت‬
‫– راه حل‪ :‬مقايسه هدف فعلي با تمام اهداف موجود در پشته‬
‫• ناكارا به دليل زيرهدف هاي تكراي (چه موفقيت و چه‬
‫شكست)‬
‫– راه حل‪ :‬ذخيره نتايج قبلي (با مصرف حافظه بيشتر) – نوعي‬
‫‪memorization‬‬
‫• به طور گسترده اي در برنامه نويسي منطقي استفاده مي‬
‫‪32‬شود‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫رزولوشن‪ :‬خالصه‬
‫• رزولوشن در منطق مرتبه اول‬
‫• فرض مي شود كه دو ‪ clause‬استاندارد شده اند به گونه اي‬
‫كه شامل متغير يكساني نباشند‪.‬‬
‫‪Apply resolution steps to CNF(KB  α); complete for FOL‬‬
‫‪33‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫تبديل به ‪CNF‬‬
‫‪34‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫تبديل به ‪CNF‬‬
‫‪35‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬
‫اثبات بوسيله رزولوشن‪ :‬مثال‬
‫‪36‬‬
‫دانشگاه صنعتي اصفهان دانشکده برق و کامپيوتر‬

similar documents