Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

อัลกอริทึมสำหรับ Tableau \ (\ mathcal {ALC} \) satisfiablity แนวคิด - ตัวอย่างที่ 1

เราตรวจสอบว่า \ (C = (A \ sqcap \ NEG) \ sqcup B \) พอใจ มันมีอยู่ใน NNF ดังนั้นเราโดยตรงสามารถใช้อัลกอริทึมฉากไป

\[(A \sqcap \neg A) \sqcup B.\]

กฎเฉพาะคือ \ (\ sqcup \ ข้อความ {กฎ} \) เรามีสองเป็นไปได้ ประการแรกเราสามารถลอง

\[L(x)=\{C, A \sqcap \neg A\}.\]

แล้วเราสามารถใช้ \ (\ sqcap \ ข้อความ {กฎ} \) และได้รับ

\[L(x)=\{C, A \sqcap \neg A, A, \neg A\}.\]

เราได้รับการปะทะกันจึงเลือกนี้ไม่ประสบความสำเร็จ ประการที่สองเราสามารถลอง

\[L(x)=\{C, B\}.\]

ไม่มีกฎมากขึ้นมีผลบังคับใช้และเราได้รับการปะทะกันไม่ ดังนั้น \ ((A \ sqcap \ NEG) \ sqcup B \) พอใจ

รูปแบบ \ (\ mathcal {I} \) satisfiying มันจะได้รับโดย

\[\Delta^\mathcal{I}=\{x\}, A^\mathcal{I}=\emptyset, B^\mathcal{I}=\{x\}.\]


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.