Encyklopedia w Markpol

Reklama:

Dedukcja naturalna to bardzo intuicyjny i generujący ładne dowody system dowodzenia twierdzeń, bazowany na systemach Hilberta. Dowód to lista formuł objętych oknami. Operacje w bardzo prostej wersji to:
  • dodanie założenia, otwiera to okno
  • przepisanie dowolnego akywnego założenia
  • zamknięcie okna, dodaje się za oknem formułę "pierwsza formuła okna \supset ostatnia formuła okna", wszystkie formuły w oknie są deaktywowane
  • użycie jednej z reguł dowodzenia (w szczególności modus ponens na dowolnych aktywnych) na dowolnych aktywnych formułach. Każda formuła leżąca poza oknem, zwykle powstała w wyniku zamknięcia ostatniego okna, jest twierdzeniem. Oczywiście okna są wyłącznie graficzną reprezentacją tego co się dzieje.

    Przykład

    Udowodnijmy, że P \supset (Q \supset P).
    1. P (założenie)
    2. Q (założenie)
    3. P (przepisanie aktywnej formuły 1)

    4. Q \supset P (eliminacja założenia 2, deaktywacja 2 i 3)

    5. P \supset (Q \supset P) (eliminacja założenia 1, deaktywacja 1 i 4) Dowód tego bardzo prostego twierdzenia jest - właśnie bardzo prosty. Co nie zawsze jest prawdą w przypadku innych systemów dowodzenia.

    Bardziej rozbudowane wersje

    Przedstawiona tu wersja potrafi tylko dodawać i eliminować implikacje. Bardziej rozbudowane wersje zajmują się też innymi spójnikami dodając nowe reguły wyprowadzania formuł i zamykania okien. Zobacz też: przegląd zagadnień z zakresu matematyki

    Chcesz wypromować swoją stronę w internecie?? - nie zwlekaj pozycjonowanie w Luman.biz to rozsądny wybór
    2005 Encyklopedia
    These materials are based onWikipedia and licensed under the GNU FDL
    Credit Card|MPAA|Buy PSP|Free Advertising|Credit Card

    		•