Dedukcja naturalna
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 aktywnego założenia
- zamknięcie okna, dodaje się za oknem formułę "pierwsza formuła okna
ostatnia formuła okna", wszystkie formuły w oknie są dezaktywowane - 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.
[edytuj] Przykład
Udowodnijmy, że 
.
1. P (założenie)
|
(eliminacja założenia 2, dezaktywacja 2 i 3)
5. (eliminacja założenia 1, dezaktywacja 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.
[edytuj] 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.
