[討論] 用數位邏輯的觀點判斷論證有效性

看板logic作者FTICR (FT-ICR)時間5年前 (2018/09/08 16:11)推噓3(3推 0噓 3→)

留言6則, 3人參與討論串1/1

因為有些電資背景先學過了邏輯電路(數位邏輯)，才學基礎邏輯(通識課) 所以常常思考方式會用數位邏輯來想，兩者之間 (至少以命題邏輯，更深內容的沒學過) ，我覺得是等價的，都是以布林邏輯為基礎比如說 CNF，在數位邏輯中叫 product of sums (POS) DNF，在數位邏輯中叫 sum of products (SOP) (大部分時喜歡把電路化簡成這樣的形式) 學到有效性證明方式，各種方法像是直接、反證、條件這些，說實在用得不太習慣也常常卡住要想下一步該怎麼做所以自己把數位邏輯的觀點拿來用，用自己的方法證 (照著做一定可以證出來，不會證到一半卡住需要回過頭去想其他解法) (考試時這樣的方法老師還看不懂，從頭跟他解釋@@) 以上廢話太多，直接開始吧一個論證: P1 P2 ... Pn ── C 定義： P1ΛP2Λ...ΛPn ⊃ C如果是恆真句，則推論有效我的作法是：先對 P1ΛP2Λ...ΛPn 進行運算 (數位邏輯常做的邏輯化簡) ，可以得到S= (A1ΛB1Λ...ΛN1)Ｖ(A2ΛB2Λ...ΛN2)Ｖ(A3ΛB3Λ...ΛN3)Ｖ... Ｖ(AkΛBkΛ...ΛNk) 的形式 (DNF) 再做 ~SＶC (也就是S⊃C)的邏輯運算，如果是恆真句，則推論有效又或是邏輯運算化簡太複雜不好做，可以用填表的方式我習慣的表長得這樣： (可以是2*2~4*4 最多4個變數(假設)，更多也是可以只是會變立體的) 稱為卡諾圖(Karnaugh map, K-map) BC 00 01 11 10 A 0 1 把P1、P2...Pn的邏輯各填一個表，取交集(目的也就是做Λ)，最後的表就會是S 把表S反轉(1變0、0變1)、再加上C的表，看可不可以全部填滿1(恆真)，如果可以就是有效 (當然兩個方法是互通的可以交叉使用) 直接舉實例：論證 A≡B P1 A⊃D P2 ── ~AＶ(BΛD) C 結論 P1：A≡B = (AΛB)Ｖ(~AΛ~B) P2：A⊃D = ~AＶD S = P1ΛP2 = ((AΛB)Ｖ(~AΛ~B))Λ(~AＶD)，經過邏輯運算可以得到DNF (~AΛ~B)Ｖ(AΛBΛD)Ｖ(~AΛ~BΛD) 化簡後是S = (~AΛ~B)Ｖ(AΛBΛD) ~S = (AΛ~B)Ｖ(AΛ~D)Ｖ(~AΛB) S⊃C運算恆真的話就是有效 ~SＶC = (AΛ~B)Ｖ(AΛ~D)Ｖ(~AΛB)Ｖ(~A)Ｖ(BΛD)，此運算可以發現是恆真，所以有效換成圖的話 (0就忽略不寫) P1 = A≡B P2 = A⊃D BD BD 00 01 11 10 00 01 11 10 A 0 1 1 A 0 1 1 1 1 1 1 1 1 1 1 S是P1、P2的交集就是 S ~S BD BD 00 01 11 10 00 01 11 10 A 0 1 1 A 0 1 1 1 1 1 1 1 1 (用算的結果：S = (~AΛ~B)Ｖ(AΛBΛD) 相同) C = ~AＶ(BΛD) S⊃C = ~SＶC 全都填滿1，恆真所以有效 BD BD 00 01 11 10 00 01 11 10 A 0 1 1 1 1 A 0 1 1 1 1 1 1 1 1 1 1 1 另外舉例論證 A≡B P1 A⊃D P2 ── ~B C1 結論 S⊃C運算 ~SＶC = (AΛ~B)Ｖ(AΛ~D)Ｖ(~AΛB)Ｖ(~B)=(~A)Ｖ(~B)Ｖ(~D) ，此運算非恆真，所以無效用圖去看 C1 ~B S⊃C = ~SＶC 沒填滿，非恆真所以無效 BD BD 00 01 11 10 00 01 11 10 A 0 1 1 A 0 1 1 1 1 1 1 1 1 1 1 1 再舉個例子 (#1Ip6u3En (logic)，裡面花了快30步...) AvB P1 (A&B)→~C P2 (A&~B)→D P3 (~A&B)→E P4 C→(DvE) 結論 = (~C)Ｖ(D)Ｖ(E) P1ΛP2 = (AΛ~B)Ｖ(AΛ~C)Ｖ(~AΛB) 再ΛP3 = (~AΛB)Ｖ(BΛ~C)Ｖ(AΛ~BΛD) 再ΛP4 = (AΛ~BΛD)Ｖ(AΛBΛ~C)Ｖ(~AΛBΛE)=S S⊃結論 ~S = (AΛBΛC)Ｖ(~AΛ~B)Ｖ(~AΛ~E)Ｖ(~BΛ~D) 再Ｖ (~C)Ｖ(D)Ｖ(E) 可以發現恆真，所有有效個人覺得這樣做簡單很多，不知道這樣的方式大家看得懂嗎? -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 140.112.77.199 ※ 文章網址: https://www.ptt.cc/bbs/logic/M.1536394262.A.8F2.html

推

tzudata

09/11 09:02, 5年前 , 1^F

09/11 09:02, 1^F

推

Tangut

09/12 09:12, 5年前 , 2^F

09/12 09:12, 2^F

感謝兩位板友！ ※ 編輯: FTICR (140.112.73.30), 09/14/2018 03:28:22

推

nalthax

10/20 21:49, 5年前 , 3^F