Tableau (system dowodzenia twierdzeń)

Z Wikipedii, wolnej encyklopedii
Przejdź do nawigacji Przejdź do wyszukiwania

Tableau (l. mn. tableaux) – system automatycznego dowodzenia twierdzeń polegający na konstruowaniu „drzewa” – w jego korzeniu umieszczamy formułę, której sprzeczność chcemy wykazać, mianowicie zaprzeczenie formuły, której tautologiczność chcemy wykazać.

Następnie na końcu dowolnej „gałęzi”:

  • jeśli w jakimkolwiek miejscu „gałęzi” mamy , możemy dodać ,
  • jeżeli w „gałęzi” znajduje się , możemy umieścić , a pod nim ,
  • gdy w pewnej części „gałęzi” jest , możemy wstawić rozgałęzienie: z jednej strony, z drugiej,
  • ...,
  • itd., w zależności od logiki.

Jeśli w dowolnej „gałęzi”, dla dowolnego , jest jednocześnie i , oznacza to, iż otrzymaliśmy sprzeczność i gałąź ta jest zamknięta, a więc możemy pominąć tę gałąź w dalszych rozważaniach. Jeśli zamknęliśmy wszystkie gałęzie, oznacza to, że dana formuła jest sprzeczna.