Suy luận logic và chứng minh định lý

Suy luận logic và chứng minh định lý liên quan đến việc sử dụng logic hình thức để biểu diễn tri thức và tự động hóa suy diễn, rút ra các kết luận tất yếu từ một tập hợp các tiền đề.

Definition

Chứng minh định lý là quá trình tự động suy ra liệu một công thức logic có suy ra từ một tập hợp các tiên đề hay không, thường bằng cách thao tác các công thức với các quy tắc suy luận đúng đắn cho đến khi đạt được mục tiêu hoặc một mâu thuẫn được tìm thấy.

Scope

Chủ đề này bao gồm suy luận trong logic mệnh đề và logic bậc nhất, cùng với các thuật toán tự động hóa chúng: kiểm tra tính thỏa mãn dựa trên bảng chân trị và DPLL cho logic mệnh đề, hợp nhất (unification) và nguyên lý phân giải (resolution principle) cho logic bậc nhất, suy luận tiến (forward chaining) và suy luận lùi (backward chaining), và các nền tảng của lập trình logic. Nó đề cập đến tính đúng đắn (soundness), tính đầy đủ (completeness) và tính quyết định được (decidability) của các thủ tục suy luận. Suy luận chấp nhận sự không chắc chắn hoặc mặc định được đề cập trong các chủ đề liên quan về suy luận dưới sự không chắc chắn và suy luận phi đơn điệu (nonmonotonic reasoning).

Core questions

• Điều gì có nghĩa khi một kết luận được suy ra từ một tập hợp các tiền đề, và làm thế nào để kiểm tra sự suy ra đó một cách cơ học?
• Nguyên lý phân giải, với sự hợp nhất, cung cấp một quy tắc suy luận đầy đủ duy nhất cho logic bậc nhất như thế nào?
• Suy luận tiến và suy luận lùi khác nhau như thế nào với tư cách là các chiến lược suy luận?
• Giới hạn của suy luận tự động là gì, khi tính hợp lệ bậc nhất chỉ có thể bán quyết định được (semi-decidable)?

Key concepts

• logic mệnh đề và logic bậc nhất
• suy ra và tính hợp lệ
• hợp nhất (unification)
• phân giải (resolution) và bác bỏ (refutation)
• DPLL và giải quyết SAT
• suy luận tiến (forward chaining) và suy luận lùi (backward chaining)
• mệnh đề Horn và lập trình logic
• tính đúng đắn (soundness) và tính đầy đủ (completeness)

Key theories

Nguyên lý phân giải

Phân giải của Robinson là một quy tắc suy luận duy nhất trên các mệnh đề mà, kết hợp với hợp nhất, là đầy đủ về mặt bác bỏ cho logic bậc nhất: bất kỳ tập hợp các mệnh đề không thỏa mãn nào cũng có thể được chứng minh là không thỏa mãn bằng cách suy ra mệnh đề rỗng.

DPLL và tính thỏa mãn mệnh đề

Thủ tục Davis-Putnam và sự tinh chỉnh DPLL của nó quyết định tính thỏa mãn mệnh đề bằng cách phân chia trường hợp có hệ thống với sự lan truyền đơn vị (unit propagation) và loại bỏ ký tự thuần túy (pure-literal elimination), tạo thành nền tảng của các bộ giải SAT hiện đại.

Lập trình logic và suy luận lùi

Hạn chế logic bậc nhất thành các mệnh đề Horn và giải quyết các mục tiêu theo hướng lùi tạo ra lập trình logic, trong đó tính toán là tìm kiếm chứng minh, cung cấp cả một phương pháp suy luận và một mô hình lập trình.

Clinical relevance

Chứng minh định lý tự động và giải quyết SAT/SMT được sử dụng trong xác minh phần cứng và phần mềm, phân tích chương trình, lập kế hoạch và toán học, trong khi các ngôn ngữ lập trình logic như Prolog áp dụng suy luận lùi vào cơ sở dữ liệu, phân tích cú pháp và các hệ thống dựa trên quy tắc.

History

Các thủ tục chứng minh ban đầu của Gilmore, Davis và Putnam (1960) đã tự động hóa suy luận mệnh đề và suy luận định lượng, và nguyên lý phân giải của Robinson (1965) đã hợp nhất suy luận bậc nhất thành một quy tắc duy nhất. Thập niên 1970 chứng kiến sự tinh chỉnh của phân giải thành lập trình logic và Prolog; giải quyết SAT và SMT sau đó đã phát triển thành một công nghệ thực tiễn quan trọng.

Key figures

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

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

Nguyên lý phân giải là gì?

Phân giải là một quy tắc suy luận duy nhất lấy hai mệnh đề chứa các ký tự bổ sung và tạo ra một mệnh đề mới kết hợp phần còn lại. Áp dụng lặp đi lặp lại với hợp nhất, nó có thể chứng minh rằng một tập hợp các mệnh đề bậc nhất là không thỏa mãn, đây là cơ sở để chứng minh các định lý bằng cách bác bỏ.

Chứng minh định lý tự động có được đảm bảo kết thúc không?

Đối với logic mệnh đề, tính hợp lệ có thể quyết định được, vì vậy các thủ tục sẽ kết thúc. Đối với logic bậc nhất đầy đủ, tính hợp lệ chỉ có thể bán quyết định được: một bộ chứng minh đầy đủ cuối cùng sẽ xác nhận bất kỳ công thức hợp lệ nào, nhưng có thể chạy mãi mãi trên một công thức không hợp lệ, vì vậy việc kết thúc không được đảm bảo nói chung.