To pytanie dotyczy logiki zdań i wszystkie wystąpienia „rozstrzygania” należy interpretować jako „rozstrzyganie zdań”.
To pytanie jest bardzo proste, ale od dłuższego czasu mnie niepokoi. Widzę, że ludzie twierdzą, że rozwiązanie zdań jest kompletne, ale widzę też, że ludzie twierdzą, że rozwiązanie jest niepełne. Rozumiem sens niepełnej rozdzielczości. Rozumiem również, dlaczego ludzie mogą twierdzić, że jest kompletny, ale słowo „kompletny” różni się od sposobu, w jaki używa się go „opisując naturalne odliczenie lub rachunek różniczkowy”. Nawet kwalifikator „zakończone odrzucenie” nie pomaga, ponieważ formuły muszą znajdować się w CNF, a przekształcenie formuły w równoważną formułę CNF lub równoważną formułę CNF poprzez transformację Tseityny nie jest uwzględniane w systemie dowodu.
Solidność i kompletność
Przyjmijmy ustawienie klasycznej logiki zdaniowej z relacją między jakimś wszechświatem struktur a zbiorem formuł i klasycznym Tarskimskim pojęciem prawdy w strukturze. Piszemy jeśli jest prawdziwe we wszystkich rozważanych strukturach. również systemowy system do uzyskiwania formuł z formuł.⊨ φ φ ⊢
System jest dźwięk w stosunku do jeśli kiedykolwiek mamy , mamy także . System jest kompletny w odniesieniu do jeśli kiedykolwiek mamy , mamy również .⊨ ⊢ φ ⊨ φ ⊢ ⊨ ⊨ φ ⊢ φ
Reguła rozstrzygania
Dosłowność to twierdzenie atomowe lub jego negacja. Klauzula jest rozłączeniem literałów. Formuła w CNF jest połączeniem zdań. Reguła rozstrzygania tego potwierdza
Reguła rozstrzygania stwierdza, że jeśli połączenie klauzuli z klauzulą jest zadowalające, klauzula musi być również zadowalająca.¬ p ∨ D C ∨ D
Nie jestem pewien, czy sama reguła rozstrzygania może być rozumiana jako system dowodowy, ponieważ nie ma reguł wprowadzania formuł. Zakładam, że potrzebujemy przynajmniej reguły hipotezy, która umożliwia wprowadzenie klauzul.
Niekompletność rozdzielczości
Wiadomo, że rozdzielczość jest dźwiękoszczelnym systemem. Czyli, jeśli możemy czerpać klauzuli ze wzoru stosując rozdzielczość, a następnie . Rozdzielczość jest także całkowitym odrzuceniem, co oznacza, że jeśli mamy , możemy uzyskać z za pomocą rozdzielczości.F ⊨ F.⊨ F.⊥ F.
Rozważ formułę
ψ : = p ∨ q i .
W systemie Gentzen LK lub przy użyciu naturalnej dedukcji mogę wywnioskować implikację całkowicie w systemie dowodowym. Nie mogę wywnioskować tej implikacji przy użyciu rozdzielczości, ponieważ jeśli zacznę od , nie będzie żadnych rozwiązań.φ
Widzę, jak mogę udowodnić ważność tej implikacji za pomocą rozwiązania:
- Rozważ formułę
- Przekształć powyższy wzór w CNF, stosując standardowe reguły dystrybucji lub transformację Tseityny
- Wyprowadź z przekształconej formuły przy użyciu rozdzielczości.
To podejście jest dla mnie niezadowalające, ponieważ wymaga ode mnie wykonania kroków (1) i (2), które są poza systemem kontroli rozdzielczości. Wydaje się więc, że istnieje bardzo wyraźny sens, w którym rozdzielczość nie jest kompletna w sposób, w jaki mówimy, że naturalna dedukcja lub sekwencyjne rachunki są kompletne.
pytania
Biorąc powyższe pod uwagę, moje pytania są następujące:
- Jaki system dowodowy jest brany pod uwagę przy omawianiu rozwiązania? Czy to tylko reguła rozdzielczości? Jakie są inne zasady?
- Wydaje mi się bardzo jasne, że rozdzielczość nie jest kompletna w tym sensie, że naturalne odliczenie i kolejne rachunki są kompletne. Czy literatura stwierdzająca, że rozwiązanie jest kompletną terminologią nadużyć tylko dlatego, że sens, w którym rozwiązanie jest zakończone, jest bardziej interesujący niż sens, w którym jest niepełny?
- Czy ta różnica w pojęciach kompletności w odniesieniu do rozwiązania i innych kwestii oraz jak je pogodzić została omówiona bardziej szczegółowo w literaturze?
- Zdaję sobie również sprawę z tego, że rozdzielczość można sformułować w ramach kolejnych rachunków pod względem reguły cięcia. Czy „słuszny” dowód teoretyczny rozdzielczości jest taki, że jest to fragment rachunku różniczkowego, który wystarcza do sprawdzenia poprawności formuł w CNF?
Odpowiedzi:
Jaki system dowodowy jest brany pod uwagę przy omawianiu rozwiązania? Czy to tylko reguła rozdzielczości? Jakie są inne zasady?
Rozwiązanie omawiam w kontekście „klauzul”, które są sekwencjami złożonymi wyłącznie z literałów . Klasyczna klauzula wyglądałaby jak Ale możemy ją również zapisać jako
LK ograniczony do klauzul ma tylko cztery reguły wnioskowania:
Oczywiste jest, że te cztery reguły są kompletne do dedukcji klauzul, tj.
Propozycja 1 Dla każdego pkt i zestaw klauzul S mamy S ⊨ C tylko wtedy, gdy S ⊢ C .do S. S.⊨ C. S.⊢ C.
Oczywiste jest, że wtedy i tylko wtedy, gdy . Nasz system czterech reguł jest nadal odpowiedni do udowodnienia przekonwertowanego problemu, ale zauważamy, że nie potrzebujemy już tożsamości i osłabiania. Pozostałe dwie zasady nazywane są „procedurą potwierdzającą rozdzielczość”.S.⊢ C. S.∪N(C) ⊢ ⊥
Twierdzenie 2 Dla każdej klauzuli i zestawu klauzul mamydo S. S.⊨ C. wtedy i tylko wtedy, gdy używa tylko cięcia i skurczu.S.∪N(C) ⊢ ⊥
Problem konwersji problemu na dowody odrzucenia jest dwojaki:
Czy „słuszny” dowód teoretyczny rozdzielczości jest taki, że jest to fragment rachunku różniczkowego, który wystarcza do sprawdzenia poprawności formuł w CNF?
W rzeczy samej!
źródło
1)
Jedyną regułą niestrukturalną jest rozdzielczość (atomów).
Jednak sama reguła nie daje systemu dowodowego. Zobacz część 3.
2)
O ile istnieje „ładne” tłumaczenie z jednego języka na inny, możemy mówić o kompletności. Najważniejsze jest to, że możemy tłumaczyć formuły z jednego na drugi i na odwrót, skutecznie. Możesz sprawdzić tezę Roberta Reckhow'a, w której zajmuje się kwestią łączności i pokazuje, że w systemach Frege długość dowodów nie zmienia się bardziej niż wielomian, więc w pewnym sensie można wybrać dowolny zestaw odpowiednich łączników, które ci się podobają.
Sytuacja dla rozwiązania jest podobna. Poprzez redukcję z SAT do 3SAT możemy ograniczyć naszą uwagę do CNF, a transformacja może być wykonana bardzo skutecznie.
Zwróć uwagę, że tutaj nie ma rozwiązania problemu, problem dotyczy także innych systemów sprawdzających. Weźmy na przykład Frege o ograniczonej głębokości, gdzie głębokość formuł musi być ograniczona stałą, więc z definicji nie może udowodnić żadnych rodzin formuł o nieograniczonej głębokości.
3)
Definicja jest bardzo ogólna i wcale nie mówi o strukturze dowodu. Wszystko, co spełnia te warunki, jest systemem dowodu zdaniowego.
Jaką klasę formuły powinniśmy wziąć pod uwagę w tych przedmiotach? Rozważono różne klasy formuł, a pierwszym podejściem do znanego mi problemu jest teza Roberta Reckhow'a, w której pokazuje on, że dopóki interesuje się systemami Frege, nie ma znaczenia, jakiego odpowiedniego zestawu łączników używa każdy z nich są równoważne.
Jeśli chodzi o rozdzielczość, jeśli naprawdę chcemy mieć kompletność wszystkich formuł, a nie tylko CNF, można bez problemu włączyć stałe tłumaczenie wielomianowe z dowolnych formuł do CNF, ponieważ tłumaczenie jest obliczalne w czasie wielomianowym.
4)
Rozdzielczość jest w porządku, ale tak też można myśleć o tym, jak wspomniałeś, tj. Możemy oczywiście traktować ją jako zasadę cięcia, gdy formuła cięcia jest dodatnimi atomami, przenosząc atomy ujemne do poprzednika i utrzymując pozytywne w sukcesie:
ps: Moja odpowiedź pochodzi głównie z teoretycznej złożoności dowodu. Możesz sprawdzić inne perspektywy, takie jak teoria dowodu strukturalnego .
Bibliografia:
źródło