Jakie były wady procedury rozwiązywania problemów Robinsona?
Paulson i wsp. Od LCF do Isabelle / HOL powiedz:
Rozwiązanie logiki pierwszego rzędu, w zasadzie kompletne, ale w praktyce często rozczarowujące.
Myślę, że kompletność oznacza, że mogą udowodnić poprawność każdej prawdziwej formuły w logice pierwszego rzędu. W Handbook of Automated Reasoning znajduję:
Rozdzielczość jest całkowicie kompletną metodą dowodzenia twierdzeń: sprzeczność (tj. Klauzula pusta) może zostać wydedukowana z dowolnego niezadowalającego zbioru klauzul.
Z Wikipedii:
Próba udowodnienia, że formuła pierwszego rzędu jest niezadowalająca, może skutkować niezakończonymi obliczeniami
Dlaczego to rozczarowuje?
Odpowiedzi
Podczas gdy „rozczarowujące w praktyce” na pewno nie jest definiowane formalnie, w przeciwieństwie do „pełna” (co robi rzeczywiście myśli „może ostatecznie okazać się każdy prawdziwy wzór”), to dość łatwo znaleźć przykłady, gdzie naiwni rozdzielczości nie jest nawet odpowiednia, tj przykładów, które powinny być łatwe do udowodnienia, ale która rozdzielczość jest bardzo wolna.
Znanym przykładem jest kodowanie zasady gołębnika dla$n$ dziury w logice zdań (czyli stwierdzeniem „$n+1$ gołębie nie mogą się zmieścić $n$otwory bez duplikatów). Nie ma dowodu na to stwierdzenie, używając tylko rozdzielczości w czasie podwykładniczej w$n$.
Jeszcze gorzej jest w logice predykatów, gdzie bardzo łatwo jest znaleźć instrukcje bez żadnych dowodów szybkiego rozstrzygnięcia.
Zauważ, że każda implementacja rozdzielczości musi implementować strategię doboru rozdzielczości, co już jest bardzo trudnym problemem i aktywnym obszarem badań, ponieważ większość praktycznych algorytmów dowodzenia twierdzeń to ulepszenia naiwnej rozdzielczości, np. Hiper-rozdzielczość .