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} \) TBoxes

เราขยายฉากอัลกอริทึมในการตรวจสอบ satisfiability ของ \ (\ mathcal {ALC} \) TBoxes

  • \ (\ mathcal {ALC} \) TBox มีหลักการอย่างเดียว (GCIs) ของฟอร์ม \ (C \ sqsubseteq D \) (หมายเหตุที่สัจพจน์ของฟอร์ม \ (C \ equiv D \) สามารถเขียนใหม่เป็น \ (C \ sqsubseteq D \) และ \ (D \ sqsubseteq C \))
  • GCI ทุกเทียบเท่ากับ \ (\ \ top sqsubseteq \ NEG C \ sqcup D \)

เราสามารถ internalize TBox ทั้งหมดเป็นความจริงเดียว:

\[\mathcal{T}=\{C_i \sqsubseteq D_i | 1 \leq i \leq n\}\]

เทียบเท่ากับ

\[ \top \sqsubseteq \underset{1 \leq i \leq n}{{\LARGE\sqcap}} \neg C_i \sqcup D_i \]

ปล่อย \ (C_ \ mathcal {T} \) เป็นแนวความคิดทางด้านขวาของ GCI แล้วกฎเพิ่มเติมคือ

\ (\ mathcal {T} \) กฎ ถ้า \ (C_ \ mathcal {T} \, \, \ ไม่ได้ \ in L (V), \ text {บาง} \ v ใน V \)
แล้วก็ \ (L (V) = L (V) \ ถ้วย \ {C_ \ mathcal {T} \} \)

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.