Odrębne zmienne dla różnych klauzul

W dowodzeniu twierdzenia o rozdzielczości zwykle przyjmuje się, że zmienne w różnych klauzulach są różne. To nie dzieje się automatycznie; do wdrożenia wymaga znacznego dodatkowego kodu i obliczeń. Biorąc to pod uwagę, szukam dla niego skrzynki testowej.

Problem polega na tym, że we wszystkich testowanych dotychczas testach nie ma to znaczenia. Przypuszczalnie ma to znaczenie tylko w nietypowych przypadkach krawędzi. Jak to ujęła Wikipedia , „zmienne w różnych klauzulach są różne ... Teraz, ujednolicenie Q (X) w pierwszej klauzuli z Q (Y) w drugiej klauzuli oznacza, że X i Y i tak stają się tą samą zmienną”.

Czy są jakieś znane przypadki testowe, które faktycznie dadzą złą odpowiedź, jeśli różne klauzule będą używać tych samych zmiennych?

logic automated-theorem-proving

— rwallace
źródło

Edycja: znalazłem lepszy przykład. Rozważ następujące klauzule: Oczywiście ten zestaw klauzul jest sprzeczny. Bez zmiany nazwy zmiennych, jest możliwe tylko rezolwenta i nie więcej rezolwenty możliwe - prowadzą do podstawienia dla , który jest niemożliwy.

\begin{aligned} \neg P (x) \lor P (f (x)) \\ P (x) \\ \neg P (f (f (x))) \end{aligned}

$\begin{align} & \lnot P(x) \lor P(f(x)) \\ & P(x) \\ & \lnot P(f(f(x)))\\ \end{align}$

P (f (x))

$P(f(x))$

f (x)

$f(x)$

x

$x$

Edycja: Rozważ znaczenie klauzul. Każda klauzula jest domyślnie kwantyfikowana uniwersalnie. Zatem znaczenie jego zmiennych nie jest ustalone na niczym. Powiedzmy teraz, że masz dwie klauzule zawierające . Jeśli wykonujesz rozdzielczość bez zmiany nazwy w jednym z nich, dodajesz do znaczenie, którego nie ma: mówisz, że oznacza to samo w obu klauzulach, co nie jest prawdą. Jeśli nie masz odrębnych zmiennych w swoich klauzulach, rozwiązanie da ci zbyt słabe wnioski. $x$ $x$ $x$ $x$

(Oryginalna odpowiedź.) Załóżmy na przykład 4 klauzule:

$A\lor B(x)$
$\lnot A\lor C(x)$
$\lnot B(c)$
$\lnot C(d)$

$x, y$ $c, d$ $x$ $B(x)\lor C(x)$ $\lnot B(c)$ $C(c)$ $\lnot C(d)$

Z drugiej strony, jeśli zmienimy nazwę na w drugim, aby mieć rozłączny zestaw zmiennych, otrzymamy z pierwszego kroku rozwiązywania i możemy uzyskać pustą klauzulę za pomocą i . $x$ $y$ $B(x)\lor C(y)$ $\lnot B(c)$ $\lnot B(d)$

— Petr Pudlák
źródło

Kiedy próbuję tego w moim prover z wyłączonymi odrębnymi zmiennymi, rozwiązuje z aby dać , podobnie uzyskuje i stąd pustą klauzulę, więc wynik końcowy jest taki sam. Czy coś brakuje?

B (x)

$B(x)$

\neg B (c)

$\lnot B(c)$

A

$A$

\neg A

$\lnot A$

— rwallace

@rwallace Brak odrębnych zmiennych nie oznacza, że nie można wyprowadzić pustej klauzuli, tylko że metody nie są kompletne. Jeśli zawsze zmieniasz nazwy zmiennych, nie ma znaczenia, w jakiej kolejności wybierasz klauzule, zawsze wyprowadzisz pustą klauzulę, jeśli oryginalny zestaw jest niezadowalający - metoda jest kompletna. Ale jeśli nie zmienisz nazw zmiennych, wtedy (jak pokazuje przykład) kolejność ma znaczenie nagle - niektóre sekwencje pochodnych nie znajdą pustej klauzuli. I też nie może powiedzieć z góry, która sekwencja pochodnych jest właściwa.

— Petr Pudlák,

Ale czy nie jest tak, że kompletna metoda musi ostatecznie wypróbować każdą możliwą pochodną (chyba że najpierw znajdzie pustą klauzulę)? Aby mieć pewność, że nie ma gwarancji, wypróbuje wyprowadzenia, o których wspomniałem wcześniej, niż te, o których wspomniałeś, ale gdy te, które wymieniłeś, zawiodą z powodu braku wyraźnych zmiennych, te, o których wspomniałem, są nadal otwarte i kompletna metoda musi wrócić i spróbować te prędzej czy później?

— rwallace

Twoje uzupełnienie dotyczące znaczenia klauzul w streszczeniu ma sens, ale wydaje mi się, że jeśli tak jest, to powinno być możliwe znalezienie przypadku testowego, czegoś, co mógłbym włożyć do dowcipu i spowodować, że udzieli on złej odpowiedzi, jeśli funkcja odrębnych zmiennych jest wyłączona. Po prostu nie udało mi się znaleźć takiego przypadku testowego.

— rwallace

@rwallace Dlaczego chcesz to zrobić? Rozwiązanie jest kompletną metodą i wiesz, że w każdych okolicznościach konieczne jest wykonanie rozstrzygania każdej pary klauzul tylko raz. Sugerujesz, aby w końcu wypróbować wszystkie możliwe sekwencje, jak kontynuować cofanie. Spowoduje to naprawdę ogromny wzrost złożoności algorytmu, nawet nie porównywalny z prostą zmianą nazw zmiennych na każdym etapie.

— Petr Pudlák,