• Artykuły
  • Forum
  • Ciekawostki
  • Encyklopedia
  • Forma preneksowa

    Przeczytaj także...
    Kwantyfikator – termin przyjęty w matematyce i logice matematycznej na oznaczenie zwrotów: dla każdego, istnieje takie i im pokrewnych, a także odpowiadającym im symbolom wiążacym zmienne w formułach. Są podstawowym elementem w rozwoju logiki pierwszego rzędu.Rachunek predykatów pierwszego rzędu – (ang. first order predicate calculus) to system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu "dla każdej funkcji z X na Y ..." (gdyż funkcja jest podzbiorem X × Y), "istnieje własność p, taka że ..." czy "dla każdego podzbioru X zbioru Z ...". Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną).
    Koniunkcyjny operator binarny – konstrukcja, która ułatwia rozumowania dotyczące składni wyrażeń logicznych. Jest to dowolne wyrażenie p ∘ q {displaystyle pcirc q} , które jest spełnione dokładnie wtedy, gdy zarówno p {displaystyle p} , jak i q {displaystyle q} są w pewnym ustalonym stanie. Zależnie od operatora może to oznaczać albo pozytywne albo negatywne wystąpienie.

    Forma preneksowa (ang. prenex form lub prenex normal form) – taka postać formuły logicznej, w której wszystkie kwantyfikatory przesunięte są na początek formuły. Inna jej nazwa to przedrostkowa postać normalna.

    Każde zdanie rachunku predykatów pierwszego rzędu można sprowadzić do postaci preneksowej. Najpierw należy zmienić nazwy wszystkim zmiennym, które kolidują, na przykład: na:

    co w żaden sposób nie zmienia znaczenia formuły.

    Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) – proces, w którym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiejś teorii, często przy okazji generując jego dowód. Twierdzenia te należą zwykle do rachunku zdań lub rachunku predykatów pierwszego rzędu.

    Następnie należy przenosić kwantyfikatory coraz wyżej, zmieniając je na przeciwny za każdym razem, gdy napotkają negację:

    Jeśli czy też i nie występuje w (co sobie zagwarantowaliśmy zmieniając nazwy wszystkich kolidujących zmiennych), przeniesienie kwantyfikatora wyżej nie zmienia znaczenia formuły. Można to uogólnić na ogólny operator koniunkcyjny i dysjunkcyjny.

    Forma preneksowa jest bardzo wygodna dla komputera, w mniejszym zaś stopniu dla ludzi.

    Przykłady[ | edytuj kod]

  • jest w formie preneksowej
  • nie jest w formie preneksowej.




  • Reklama

    Czas generowania strony: 0.032 sek.