Những thiếu sót trong thủ tục giải quyết của Robinson là gì?

Aug 16 2020

Paulson và cộng sự. Từ LCF đến Isabelle / HOL nói:

Độ phân giải cho logic bậc nhất, hoàn chỉnh về nguyên tắc nhưng thường gây thất vọng trong thực tế.

Tôi nghĩ rằng hoàn chỉnh có nghĩa là họ có thể chứng minh bất kỳ công thức đúng nào theo logic bậc nhất là đúng. Trong Sổ tay lý luận tự động, tôi tìm thấy:

Giải quyết là một phương pháp chứng minh định lý hoàn chỉnh về mặt phản biện: một mâu thuẫn (tức là mệnh đề trống) có thể được suy ra từ bất kỳ tập hợp mệnh đề không thỏa mãn nào.

Từ Wikipedia:

Cố gắng chứng minh một công thức bậc nhất thỏa mãn nhưng không thỏa mãn có thể dẫn đến một phép tính liên tục

Why is that disappointing?

Trả lời

1 cody Aug 20 2020 at 00:26

While "disappointing in practice" is certainly not definable formally, unlike "complete" (which does indeed mean "can eventually prove every true formula"), it's pretty easy to find examples where naive resolution is not even remotely adequate, i.e. examples which should be easy to prove but which resolution is extremely slow on.

A famous example is an encoding of the pigeon hole principle for $n$ holes in propositional logic (which is the statement "$n+1$ pigeons cannot fit in $n$ holes without duplicates). There is no proof of this statement using only resolution in time sub-exponential in $n$.

Things are even worse in predicate logic, where it is very easy to find statements without any fast resolution proofs.

Note that any implementation of resolution must implement a strategy for picking the resolvents, which is already a very difficult problem, and an active area of research, since most practical algorithms for theorem proving are enhancements of naive resolution, e.g. hyper-resolution.