4.1 ຕັກກະປະພົດ ແລະ ການອະນຸມານ
ໄວຍາກອນ, ຄວາມໝາຍ, ຕາຕະລາງຄ່າຄວາມຈິງ, resolution ແລະ Horn clauses.
ຕັກກະປະພົດ (propositional logic)
ປະພົດ ແມ່ນປະໂຫຍກທີ່ ຈິງ (T) ຫຼື ບໍ່ຈິງ (F). ເຊື່ອມດ້ວຍ: ¬ (ບໍ່), ∧ (ແລະ), ∨ (ຫຼື), → (ຖ້າ...ແລ້ວ), ↔ (ກໍຕໍ່ເມື່ອ).
| P | Q | P → Q |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
ບັນຫາການໃຫ້ເຫດຜົນ
ໃຫ້ ຖານຄວາມຮູ້ KB ແລະ ປະໂຫຍກ α: KB ສົ່ງຜົນ (entails) α ບໍ? (KB ⊨ α)
- ຕາຕະລາງຄ່າຄວາມຈິງ: ກວດທຸກກໍລະນີ — ຖືກຕ້ອງ ແຕ່ 2ⁿ ແຖວ.
- ກົດ resolution: ຈາກ (A ∨ B) ແລະ (¬B ∨ C) → (A ∨ C). ປ່ຽນ KB ∧ ¬α ເປັນ CNF ແລ້ວ resolve ຈົນໄດ້ປະໂຫຍກຫວ່າງ → ພິສູດໄດ້.
- ປະໂຫຍກ Horn (ມີ literal ບວກບໍ່ເກີນ 1, ເຊັ່ນ A ∧ B → C) + modus ponens: - ອະນຸມານໄປໜ້າ (forward chaining): ເລີ່ມຈາກຂໍ້ເທັດຈິງ, ໃຊ້ກົດໄປເລື້ອຍໆ ຈົນໄດ້ α. - ອະນຸມານຖອຍຫຼັງ (backward chaining): ເລີ່ມຈາກ α, ຊອກກົດທີ່ສະຫຼຸບ α, ພິສູດເງື່ອນໄຂຂອງມັນ.
ຕົວຢ່າງ
KB: ຝົນຕົກ → ດິນປຽກ, ດິນປຽກ → ລື່ນ, ຝົນຕົກ.
Forward chaining: ຝົນຕົກ ⇒ ດິນປຽກ ⇒ ລື່ນ ✅
ຕັກກະລຳດັບທີ 1 (first-order logic) ເພີ່ມ ຕົວແປ ແລະ ຕົວບອກປະລິມານ (∀, ∃) ແລະ ພາສາ Prolog ໃຊ້ຫຼັກ backward chaining ນີ້.
