การให้เหตุผลเชิงตรรกะและการพิสูจน์ทฤษฎีบท

การให้เหตุผลเชิงตรรกะและการพิสูจน์ทฤษฎีบทเกี่ยวข้องกับการใช้ตรรกะรูปนัยเพื่อแสดงความรู้และการทำให้การอนุมานเป็นไปโดยอัตโนมัติ โดยการสรุปผลที่จำเป็นต้องเป็นไปตามชุดของข้อสมมติฐาน

Definition

การพิสูจน์ทฤษฎีบทคือการอนุมานโดยอัตโนมัติว่าสูตรตรรกะเป็นไปตามชุดของสัจพจน์หรือไม่ โดยทั่วไปจะทำโดยการจัดการสูตรด้วยกฎการอนุมานที่ถูกต้องจนกว่าจะบรรลุเป้าหมายหรือเกิดข้อขัดแย้ง

Scope

หัวข้อนี้ครอบคลุมการให้เหตุผลในตรรกะเชิงประพจน์และตรรกะอันดับหนึ่ง รวมถึงอัลกอริทึมที่ทำให้เป็นไปโดยอัตโนมัติ: การตรวจสอบความพึงพอใจโดยใช้ตารางค่าความจริงและ DPLL สำหรับตรรกะเชิงประพจน์, การรวมกันและหลักการการแยก (resolution principle) สำหรับตรรกะอันดับหนึ่ง, การเชื่อมโยงไปข้างหน้าและข้างหลัง (forward and backward chaining), และรากฐานของการเขียนโปรแกรมเชิงตรรกะ (logic programming) นอกจากนี้ยังกล่าวถึงความถูกต้อง (soundness), ความสมบูรณ์ (completeness), และความสามารถในการตัดสินใจ (decidability) ของกระบวนการอนุมาน การให้เหตุผลที่ยอมรับความไม่แน่นอนหรือค่าเริ่มต้นจะถูกกล่าวถึงในหัวข้อที่เกี่ยวข้องกับการให้เหตุผลภายใต้ความไม่แน่นอนและการให้เหตุผลแบบไม่เป็นมอนอโทนิก (nonmonotonic reasoning)

Core questions

• การที่ข้อสรุปหนึ่งถูกอนุมานได้จากชุดของข้อสมมติฐานหมายความว่าอย่างไร และจะตรวจสอบการอนุมานนั้นด้วยกลไกได้อย่างไร?
• หลักการการแยก (resolution principle) ร่วมกับการรวมกัน (unification) ให้กฎการอนุมานที่สมบูรณ์เพียงหนึ่งเดียวสำหรับตรรกะอันดับหนึ่งได้อย่างไร?
• การเชื่อมโยงไปข้างหน้า (forward chaining) และการเชื่อมโยงย้อนหลัง (backward chaining) แตกต่างกันอย่างไรในฐานะกลยุทธ์การอนุมาน?
• ข้อจำกัดของการให้เหตุผลอัตโนมัติคืออะไร เมื่อพิจารณาว่าความถูกต้องของตรรกะอันดับหนึ่งเป็นเพียงกึ่งตัดสินใจได้ (semi-decidable)?

Key concepts

• ตรรกะเชิงประพจน์และตรรกะอันดับหนึ่ง
• การอนุมานและความถูกต้อง
• การรวมกัน (unification)
• การแยก (resolution) และการหักล้าง (refutation)
• DPLL และการแก้ปัญหา SAT
• การเชื่อมโยงไปข้างหน้าและการเชื่อมโยงย้อนหลัง
• Horn clauses และการเขียนโปรแกรมเชิงตรรกะ
• ความถูกต้อง (soundness) และความสมบูรณ์ (completeness)

Key theories

หลักการการแยก (Resolution principle)

การแยกของ Robinson เป็นกฎการอนุมานเดียวบนอนุประโยค (clauses) ซึ่งเมื่อรวมกับการรวมกันแล้ว จะสมบูรณ์สำหรับการหักล้างในตรรกะอันดับหนึ่ง: ชุดของอนุประโยคที่ไม่สามารถทำให้เป็นจริงได้สามารถแสดงให้เห็นว่าไม่สามารถทำให้เป็นจริงได้โดยการอนุมานอนุประโยคว่างเปล่า

DPLL และความพึงพอใจเชิงประพจน์

ขั้นตอนวิธีของ Davis-Putnam และการปรับปรุง DPLL ตัดสินความพึงพอใจเชิงประพจน์โดยการแยกกรณีอย่างเป็นระบบด้วยการแพร่กระจายหน่วย (unit propagation) และการกำจัดตัวอักษรบริสุทธิ์ (pure-literal elimination) ซึ่งเป็นพื้นฐานของตัวแก้ปัญหา SAT สมัยใหม่

การเขียนโปรแกรมเชิงตรรกะและการเชื่อมโยงย้อนหลัง

การจำกัดตรรกะอันดับหนึ่งให้เป็น Horn clauses และการแก้เป้าหมายย้อนหลังทำให้เกิดการเขียนโปรแกรมเชิงตรรกะ ซึ่งการคำนวณคือการค้นหาการพิสูจน์ โดยให้ทั้งวิธีการให้เหตุผลและกระบวนทัศน์การเขียนโปรแกรม

Clinical relevance

การพิสูจน์ทฤษฎีบทอัตโนมัติและการแก้ปัญหา SAT/SMT ถูกนำมาใช้ในการตรวจสอบฮาร์ดแวร์และซอฟต์แวร์, การวิเคราะห์โปรแกรม, การวางแผน, และคณิตศาสตร์ ในขณะที่ภาษาการเขียนโปรแกรมเชิงตรรกะ เช่น Prolog นำการอนุมานแบบเชื่อมโยงย้อนหลังไปใช้กับฐานข้อมูล, การแยกวิเคราะห์ (parsing), และระบบที่ใช้กฎเกณฑ์

History

ขั้นตอนการพิสูจน์ในยุคแรกโดย Gilmore, Davis และ Putnam (ค.ศ. 1960) ได้ทำให้การให้เหตุผลเชิงประพจน์และเชิงปริมาณเป็นไปโดยอัตโนมัติ และหลักการการแยกของ Robinson (ค.ศ. 1965) ได้รวมการอนุมานอันดับหนึ่งเข้าเป็นกฎเดียว ในทศวรรษ 1970 การแยกได้รับการปรับปรุงให้เป็นโปรแกรมเชิงตรรกะและ Prolog; การแก้ปัญหา SAT และ SMT ได้พัฒนาเป็นเทคโนโลยีที่สำคัญในทางปฏิบัติในเวลาต่อมา

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

หลักการการแยก (resolution principle) คืออะไร?

การแยกคือกฎการอนุมานเดียวที่ใช้อนุประโยคสองชุดที่มีตัวอักษรเสริม (complementary literals) และสร้างอนุประโยคใหม่ที่รวมส่วนที่เหลือเข้าด้วยกัน เมื่อนำไปใช้ซ้ำๆ ร่วมกับการรวมกัน จะสามารถแสดงให้เห็นว่าชุดของอนุประโยคอันดับหนึ่งไม่สามารถทำให้เป็นจริงได้ ซึ่งเป็นพื้นฐานสำหรับการพิสูจน์ทฤษฎีบทโดยการหักล้าง

การพิสูจน์ทฤษฎีบทอัตโนมัติรับประกันว่าจะสิ้นสุดหรือไม่?

สำหรับตรรกะเชิงประพจน์ ความถูกต้องสามารถตัดสินใจได้ ดังนั้นขั้นตอนวิธีจะสิ้นสุด สำหรับตรรกะอันดับหนึ่งแบบเต็ม ความถูกต้องเป็นเพียงกึ่งตัดสินใจได้: ตัวพิสูจน์ที่สมบูรณ์จะยืนยันสูตรที่ถูกต้องในที่สุด แต่อาจทำงานตลอดไปกับสูตรที่ไม่ถูกต้อง ดังนั้นการสิ้นสุดจึงไม่ได้รับการรับประกันโดยทั่วไป