6-4 Inference (ii) - Simple Knowledge, Resolution and CNF (i) - Proof by Resolution, CNF Conversion, Resolution Algorithm - Propositional Logic | Coursera

企業版面向學生

瀏覽
頂級課程
登錄
免費加入

6-4 Inference (ii) - Simple Knowledge, Resolution and CNF (i) - Proof by Resolution, CNF Conversion, Resolution Algorithm

Loading...

人工智慧：搜尋方法與邏輯推論 (Artificial Intelligence - Search & Logic)

国立台湾大学

4.8（197 個評分） | 18K 名學生已註冊

本課程分為人工智慧（上）、人工智慧（下）兩部份，第一部分除了人工智慧概論外，著重在目標搜尋、meta heuristic、電腦對弈、演繹學習（包含證言邏輯、一階邏輯及 planning ）等技術。這些技術主要發展時機為人工智慧的第一波及第二波熱潮，也就是 1950 年代至 1990 年代附近的主流發展，即使到現在也在各個領域廣為應用。課程教學目標：使同學對人工智慧有基礎概念同學能夠理解如何運用目標搜尋技術及演繹學習方式達成人工智慧同學能將相關技術應用到自己的問題上

查看授課大綱

您將學習的技能

Artificial Intelligence (AI), Search Algorithm, A.I. Artificial Intelligence, Algorithms

審閱

4.8（197 個評分）

5 stars
81.21%
4 stars
14.72%
3 stars
3.55%
2 stars
0.50%

從本節課中

Propositional Logic

6-1 Logical Agents (i) - Generic Knowledge-Based Agent, PEAS16:35

6-2 Logical Agents (ii) - Logic, Entailment and Models21:19

6-3 Propositional Logic, Inference (i) - Enumeration, Validity and Satisfiability19:16

6-4 Inference (ii) - Simple Knowledge, Resolution and CNF (i) - Proof by Resolution, CNF Conversion, Resolution Algorithm18:33

6-5 Resolution and CNF (ii) - Properties of Resolution, Ground Resolution Theorem11:59

6-6 Resolution and CNF (iii) - Horn and Definite Clauses, Forward Chaining17:07

6-7 Backward Chaining, Pros and Cons of Propositional Logic10:28

教學方

于天立
副教授 (Associate Professor)

以免費的價格試聽課程

腳本

好，接下來我們看一下怎麼用proportional logic來導論我們剛剛，就是我們用entailment導的那個結論。現在是一樣的狀況，那我們用一些定義，一些symbol來表示不同的狀況。比如說，我們用Px，y來表示說，在xy這一格有pit或是沒有pit，好，那一樣用W來表示wumpus，B來表示你有沒有，有沒有感覺到breeze，就，一陣風吹來，那其實主要我們現在用的就是這幾個，那S你當然還可以定義，比如說，有沒有聞到臭味等等。那我們現在的knowledge base呢就在這一個狀態，就左邊這個圖，這個狀態的時候，是我們知道，這邊是我們給它編號，等一下我們會用到，如果我們在，這邊它在導的時候，同學可以把這個R1到R5這邊，就是放在旁邊參考一下，那麼R1的話就是我們知道，在（1，1）我們沒有，我們就是沒有pit，好，這是（1，1）沒有pit，然後我們知道在（1，1）我們也沒有感覺到breeze，然後我們在（2，1）現在這邊感覺到breeze，好，那另外一些規則我們也要放在 knowledge base裡面，也就是說，譬如說，我們在（1，1），如果感覺到breeze，意思就是說，（1，2）或（2，1）其中一個是pit，好，imply。那一樣，同理，（2，1）感覺到breeze的話，那就是周邊三格，（2，1）的話，旁邊有幾個可能，就是（1，1）可能是breeze（口誤）， pit或是，（2，2），就是這邊嘛，你如果在這邊的話，你知道這個可能是pit，這可能是pit，或這個可能是pit。好，這三個可能，好，這是我們現在的knowledge base，那我們試試看說，用我們現在的這些能不能導出，given我們這些knowledge base，我們能不能導出有用的一些資訊。那第一件事呢，我們從R2開始，rule 2開始，就是從這一格開始，這是一個 bidirectional嘛，就是這個imply後面，這個也imply前面，所以就是 A equivalent B的話，我們可以用bidirectional的elimination，就是把它，就是A equivalent B，那我們就把它改成A implies B，而且B implies A，好，如果優先序擔心的話就畫一下，這是bidirectional elimination。好，我們展成這個式子，就我們把它編號成R6，好，那從這個，我們一般來說一旦導出來任何東西，我們就是繼續加入knowledge base，就我們剛剛KB是五個，那導出R6以後， R6就是一直，rule就開始加入，繼續加入原來的KB裡面。那接下來從R6，我們可以用end elimination，就是A and B為真，那我們就知道A或是B都可以，就是我們 elimination就是砍掉一個啦，就是這個我們知道，那我們當然就知道A是真的，而且B當然也是，這兩個都可以再加入knowledge base。那我們這邊當然是利用我們的自己的智慧，我們決定要看哪一個對我們比較有用。那我們先採用這一個，就是- 這一邊，那接下來我們用contrapositive來做，就是A implies B，則，反過來就是not Ｂ imply not Ａ，就是，就這樣，這一個的not implies這一個的not，好，再來我們使用的是modus ponens，modus ponons是如果A implies B，而且我們又知道A，那我們得到的結果就是B，這是modus ponens，蠻簡單的一個rule。我們看一下，R8是這個樣嘛，我們回去看我們knowledge base裡面其實有得到這一個R4，我們知道，在B1，在（1，1）沒有breeze，所以我們就直接拿到這個結論。就是你知道一個關聯，然後就前提和結論的這個關聯，那已知這個前提就可以拿到這個結論，最後呢我們從這邊拿demogen，就是把not往裡，往裡放進來，然後把or改成and，所以我們就拿到這一個。這是我們的R式，這邊你可以再次使用 end elimination，你可以拿到兩個結論。其實你就是拿到一個，就是這個結論﹁P1，2，然後另外一個結論就是這個，﹁P2，1，好，這是我們最後的結論。我們就看到，就是，我們之前就是用interment，就是把model全部都elimination出來，拿到，如果我們現在是，如果我們講過，那蠻沒效率的，如果你的truth table，就是你involve的symbol如果非常多，假設有n個的話，基本- 上你需要 2的n次方嘛，我們involve，我們要問三個位置，那其實還好，就八個世界，我們也許這樣做得到，但是比較複雜的問題，當你有n種可能的 truthassignment的情況下，你基本上2的n次方你是做不到的。那我們如果用這些rule的話，我們可以看到，可以這樣一路演繹下來，得到我們想要的資訊。那我們剛剛這樣做，當然看起來在某些問題上也許會比較有效率，但是大家應該會有個最大的疑問，就是，就是我們剛剛我們當中有很多選擇嘛，比如說，我這一條，這邊我為什麼要bidirectional elimination，為什麼這邊要用demogen，為什麼我這邊要用modus ponens，其實都是我們的選擇，這也就是我們自己的智慧下去做的，我們當然希望的就是讓電腦能夠做到我們剛剛做的這些事情，那我們就必須有個系統化的方法來讓電腦做。那我們今天介紹一種方法，也是很實用的方法，就是resolution。好，這可能是這一整章的很重要的一個部分。你要證明用resolution來證明的時候，第一件事情你必須要先你的說想要證的東西，先把它轉化成conjunction normal form。 conjunction normal form很簡單，就是一堆disjunction的conjunction，就是一堆or的and，那我們把這些，把這其中一個我剛剛講一堆or的這個，我們成為一個clause，就是，英文的話就是子句，這邊你用子句這個想法也是Ok的，也可以這樣翻譯，就是這是一個clause，這是一個clause，它們之間是一個，and起來，這樣的形態我們稱為conjunction normal form。那如果有修過complexity那邊的同學，應該知道，如果我把一個任意的一個sentence轉換成conjunction normal form的complexity，基本上是pronominal的時間，反正多項式時間內我可以把它轉換到，那基本上你可以寫的蠻有效率，接近linear的時間。你可以把任意的sentence轉換成conjunction normal form。所以anyway，等一下我們會看到怎麼轉，但是，先跟各位講，就是讓電腦來做這件事，基本上不算很困難，好，如果你有conjunction normal form的情況下，那resolution呢，它作是什麼，是這邊是一個clause，這是一個clause，那這邊是另外一個clause，就是你已知的兩個clause，這兩個clause，當然根據conjunctive normal form定義裡面就是全部是or。那然後其中有兩個literal，它是complementary，就是互為相反。就是如果這邊有一個 P，左邊有一個P，然後右邊有一個not P，這種情況，它們其中這兩個是complementary的literal的情況下，你可以得到什麼呢，可以得到一個新的clause，那這個，這裡面就是把這兩個直接刪掉，這就是，下面就是，你把上面的元素全部抽起來，但是你可以看到這邊少了一個就是，我不是要圈那個，就是從這邊到這邊，你少了一個li，然後從這裡到這裡，你少了一個mj，就是可以直接把它們互為相反的那個literal，直接全部拿掉。舉個例子，譬如說，你如果知道這一件事情，這是一個clause，你知道這個為真，而且你知道這個為真，那你能得到的結論呢，就是你可以把這個，得到這個為真，得到這個為真的結果。這個東西要怎麼證明呢？蠻簡單的，就是truth table，你如果懷疑這件事的話，各位同學你可以試試看，你就是，我們知道A or B，然後你如果知道﹁B or C，那你可以不可以得到A or C，你要證明這件事為真，很簡單，你就是ABC才三個symbol而已，你就用truth table把就八個可能全部列出來，你就可以得到，你就會知道這個，上面這件事imply下面這件事。 Ok，這個過程，這個過程我們稱為resolution。那我們先，首先我們在探討 resolution各個特性之前，我們先看一下，就是一個比較systematical的方法，把任何一個式子改成conjunction normal form，這邊基本上經過這幾個步驟以後，一定就可以改到。第一件事情就是你的sentence裡面如果有這個bidirectional的話，你就先用bidirectional elimination，就是把它變成，剛剛有講過了，就大家還記得的話，就這個東西，你就換成 A implies B，而且B implies A。這是第一個，經過這一步以後，所有的雙箭頭全部都不見，那接下來，conjunction normal form裡面只有and或or，對不對，所以也沒有單箭頭，再下一件事就是把單箭頭拿掉，單箭頭拿掉的方式，就是contrapositive，就，contrapositive直接反過來，那這implication 的elimination，就是你這邊有寫啦，其實就是這個。就說，A α implies β，那基本上就是not α or β。好，到這一步這一步你應該就可以，經過第二步你應該就可以把所有雙箭頭還有單箭頭全部拿掉，那接下來- ，你會展，寫成一個很大的，很長的 and or 的一堆括弧的東西。好那接，再來，再來要做的事情，就是我們要把not直接往裡縮，縮進括弧裡面，然後直接接在那個literal前面。好，所以你會，把它，往裡移，那基本上這裡面過步驟，我如果合你可以，基本上是兩步啦，但是你可以把它合成一步，就是你移進來的過程就用De Ｍorgan，好。那合進來的過程，然後之後如果你遇到一個這個東西，這種出現兩次，你就用double-negation elimination。當然你有可能遇到三個、四個都有可能，那你反正兩兩你就可以拿掉，兩兩你就可以拿掉。這不會很難。所以最後你就會變成一個，經過第三步以後，你就會得到一個and or的，只有and or這種式子，然後裡面做的not全都是跟著，跟著atomic的那個symbol。 OK，就not不會在括弧外面。好，那接下來還有一件事情，就是你最後要做的事就是你把它flatten掉，因為，就是conjunction normal form就是or 跟 and嘛，所以你就把它改成那個式子，所以你只要不符合的東西你就把它either是disputed，either是把它結合交換，這都可以。利用結合律、交換律還有分配律，然後把它展成這種式子。好這過程就不會很難，我們省略幾個步驟，但是基本上就讓大家知道，電腦要做其實也差不多，原則上就是這四個步驟，我剛剛每一個步驟裡面可能再小細分成兩三個步驟，但是這個也蠻有系統，而且也有效率在多項式時間內做到。那我們，有resolution以後呢，resolution它的作用就是在 conjunc-tion normal form對不對，那我們想要證明的是什麼，我們想要證明的是KB entail α。這是我們想證的東西，那這個東，這個東西當然就很明顯地不是一個conjunction normal form。那我們要，我們利用了特性，就是 KB entails α，if and only if KB and not α，unsatisfiable，好這個，我們，大家可以回想，在前幾頁投影片裡面其實有提到。好，所以我們接下來做的事情就是反證法嘛。就是我先，你要我證這個結論，given我這個knowledge，我現在要證這個結論，有一種方法是我先假設結論是錯的，然後我設法導致矛盾，導致矛盾就是說沒有任何一個世界可以satisfy這樣的，這樣的sentence。好，那下面其實就只是一個，呃，只是一個，一個，pseudo code啦，那我們做的事情其實就是，我們先把它寫成這個樣，那你如果你的KB本身也是conjunction normal form的話，那其實，你這整個sentence全部整個sentence，因為這邊我是一個and，一個not α嘛，那這裡符合conjunction，這本身就是一個你可以視它為一個clause。所以，我要講的就是，你KB如果 conjunction normal form的話，那整個 sentence這也是一個conjunction normal form。那，裡面就很多clause。那你做的事情呢，這個algorithm做的事很單純，就是把所有兩兩的clause都去做resolution。好，那有些，有些clause可以做resolution，有些，有些clause做不出來啦。譬如說，假設說，如果你沒有那個，你如果沒有，呃，complimentary的literal的話，你就做不出來。就譬如說，你如果是 A or B，然後這是一個clause，然後另外一個clause是C or D。好，那這樣的結果你不能做任何的事情，你不能做任何resolution，reduction。那anyway，你沒關係，你就，這兩個你就可能就不去做它，好，所以簡單講你就是對所有的，在剛剛這conjunction normal form裡面所有的clause任兩兩配對，就是說如果將近有n個clause，你就Ｃn取2，全部去做這樣的事情。那能，能得到結論的就拿出來，然後，union進有的東西。好，然後這樣做直到呢，直到什麼時候，直到你，你這個的clause的數量無法再變多，沒辦法產生新的clause了。簡單講你原本已經有n個clause對不對，然後你就所有Ｃn取2，全部去做這件事情，你可能會產生一些結果，然後使得你的clause可能，譬如說原本一百個，你經過這樣做，這樣式子你可能變成一千個，而一千個一樣，你還是原則上，原則上就是你任兩兩都在做這樣的事，當然你如果剛剛原本到一百個，你就不用重覆做啦。那再做這樣的事情，然後這個clause數量又可能，可能會再增長，但是anyway，就這樣一直做，做到clause數量不再增長的情況，然後這時候如果，都還沒有出現所謂的empty clause的話，你就跟它說，原命題為假，否則你就說，原命，原命題為真。 OK，就這樣，就是empty clause是什麼東西呢？就是，什麼時會出現empty clause？也很單純，你會出現empty clause的時候就是你有個clause像是A，這樣，另外clause是﹁A。好，那這兩個你用resolution的話，你就會把同樣literal 拿掉嘛，所以你就都拿掉就變成一個empty clause。那這個empt clause意義是什麼呢？因為原本的clause裡面是or嘛，那只是它現在只有一個literal，所以它就它自己or，沒什麼，但是clause跟clause之間是用and的嘛，是and，也就是說，這個東西其實是什麼呢，是unsatisfiable。對不對？A，而且非A，這你不可能satisfy。好，也就是一個empty clause意思就是，意思就是原句， unsatisfiable。好，那這個意思就是什麼呢，KB entail α。所以我們的反證法嘛，就是我假設結論是錯的，結果矛盾，所以就是，結論必須是對的。好，那所以，如果出現這個的話，你就說原命題，就是α為真。否則，你就，你就說，你就說是false。好，我們用，一樣用剛剛那個例子，用剛剛那個例子。把KB，其實我們剛剛，這個投影片，就是換成這一個式子，其實就是原來KB的整個，換，展開的conjunction normal form。好，那我們利用這個，這個東西，我們展開的，就是我們剛剛投影片的例子，就是展開的結果是這個，這個conjunction normal form。然後加上我們在（1，1）的時候我們知道這件事。好，你就再and一個，not B（1，1）。然後我們想要得這個結論，我們看能不能，得到說，（1，2）沒有pit。好，（1，2）沒有洞，這個結論，我們做的事情就是把它再and起來，好所以我，這是原這是原來的KB，這邊三個，好，這是我們在（1，1），agent在（1，1）的時候，所新加的這個 knowledge。然後我們要試試看，證明，能不能證出（1，2）沒有洞。那我們證明方法，這個就是﹁ α。你就先假設（1，2）是有pit的，然後你去做resolution。那這邊show的是一個可能的 resolution方式，照原來pseudo code的話你要考慮要把所有兩兩全部配完。那這個圖沒有這麼大，我們沒有把所有都試完。但是我們可以舉幾個例子，比如說這兩個clause， resolve的結果就是把B（1，1），好，這個拿掉，得到這個新的，新的clause，那新的clause一樣就是加入我的，我做clause的整個集合裡面。就是原本我的clause有五個，然後做這個 resolution我clause有得到新的東西，又變六個。然後之後一樣兩兩都去做，那譬如說像這個例子裡面我們可以看到，這兩個 result的結果，你會得到這一個。好，這反正你在過程中，在call的，run的過程中你會得到。然後你再跟這個兩個， resolve的結果就會得到一個空集合。好，這意思就是說， KB and ﹁ α unsatisfiable，意思就是KB entail α ，也就是我們得到的 α，就是p，就（1，2）沒有pit這件事是真的，也就是given我們的knowledge base，它是，應該是正確的。

探索我們的目錄

免費加入並獲得個性化推薦、更新和優惠。

Coursera Footer

熱門在線課程

Finding Purpose & Meaning in Life
Understanding Medical Research
Japanese for Beginners
Introduction to Cloud Computing
Foundations of Mindfulness
Fundamentals of Finance
機器學習
使用 SAS Viya 進行機器學習
幸福科學
Covid-19 Contact Tracing
適用於所有人的人工智能課程
金融市場
心理學導論
Getting Started with AWS
International Marketing
C++
Predictive Analytics & Data Mining
UCSD Learning How to Learn
Michigan Programming for Everybody
JHU R Programming
Google CBRS CPI Training

熱門在線專項課程

Natural Language Processing (NLP)
AI for Medicine
Good with Words: Writing & Editing
Infections Disease Modeling
The Pronounciation of American English
Software Testing Automation
深度學習
零基礎 Python 入門
數據科學
商務基礎
Excel 辦公技能
Data Science with Python
Finance for Everyone
Communication Skills for Engineers
Sales Training
職業品牌管理職業生涯品牌管理
Wharton Business Analytics
Penn Positive Psychology
Washington Machine Learning
CalArts Graphic Design

在線證書

專業證書
MasterTrack 證書
Google IT 支持
IBM 數據科學
Google Cloud Data Engineering
IBM Applied AI
Google Cloud Architecture
IBM Cybersecurity Analyst
Google IT Automation with Python
IBM z/OS Mainframe Practitioner
UCI Applied Project Management
Instructional Design Certificate
Construction Engineering and Management Certificate
Big Data Certificate
Machine Learning for Analytics Certificate
Innovation Management & Entrepreneurship Certificate
Sustainabaility and Development Certificate
Social Work Certificate
AI and Machine Learning Certificate
Spatial Data Analysis and Visualization Certificate

在線學位課程

Computer Science Degrees
Business Degrees
公共衛生學位
Data Science Degrees
學士學位
計算機科學學士
MS Electrical Engineering
Bachelor Completion Degree
MS Management
MS Computer Science
MPH
Accounting Master's Degree
MCIT
MBA Online
數據科學應用碩士
Global MBA
Master's of Innovation & Entrepreneurship
MCS Data Science
Master's in Computer Science
公共健康碩士

Coursera

關於
我們提供的內容
管理團隊
工作機會
目錄
證書
MasterTrack™ 證書
學位
企業版
政府版
面向校園

社區

學生
合作夥伴
開發者
Beta 測試人員
專業譯員
博客
技術博客
教學中心

更多

條款
隱私
幫助
內容訪問
媒體
聯繫我們
目錄
附屬公司

隨時隨地學習

通過 Google Play 獲取

© 2021 Coursera Inc.保留所有權利。