Dedukcja naturalna

Rachunek kwantyfikatorów (rozdz. 3.3)

• Formuły: Ax p(x) albo ∀x p(x), Ex q(x, f(a)) albo ∃x …. Przy wpisywaniu kwantyfikator wiąże jak negacja: Ax p(x) -> q to (∀x p(x)) ⇒ q; kropka rozciąga jego zasięg do końca: Ax. p(x) -> q(x) to ∀x (p(x) ⇒ q(x)).
• Na kolokwiach i egzaminach kwantyfikator obejmuje zwykle wszystko aż do nawiasu zamykającego, dlatego aplikacja dopisuje nawiasy wszędzie tam, gdzie po kwantyfikatorze coś jeszcze stoi — np. (∃x p(x)) ⇒ ¬∀x ¬p(x).
• Symbole jak w skrypcie: zmienne u–z (z indeksem: x0 → x₀), stałe a–e i liczby (0, 42), symbole funkcyjne f–h (z argumentami, np. f(x, a)), symbole relacyjne p–t, P–S oraz φ, ψ — schematy z zadań zapisujemy jako φ(x).
• Relacje dwuargumentowe można pisać między argumentami: f(x) = y, f(x) > 0, x < y, x <= y → x ≤ y, x >= y → x ≥ y, x != y → ¬(x = y). To zwykłe symbole relacyjne — równość nie ma tu osobnych reguł. W rachunku kwantyfikatorów cyfry są stałymi, więc ⊤ i ⊥ wpisuje się jako T i F.
• Reguły (∀i) i (∃e) otwierają okno ze świeżą zmienną x₀ — aplikacja dobiera ją sama, tak by nie występowała w pozostałej części dowodu, i pilnuje, by nie była wolna w założeniach ani we wniosku. Reguła (∀e) pyta o formułę ∀x α, z której wynika cel, a (∃i) — o term-świadka t; podstawienie α[x/t] musi być dopuszczalne (Def. 52).
• Dowód w języku naturalnym jest rozumowaniem na strukturach (rozdz. 13.1): dla dowolnej struktury 𝔄 i wartościowania v pokazuje, że 𝔄 ⊨ φ[v]; oknu ze świeżą zmienną odpowiada wybór elementu uniwersum.
• Podpowiedzi działają tylko w zadaniach przykładowych na górze menu Przykłady — to zadania z kolokwiów i egzaminów, do których opublikowano rozwiązania. Pozostałe zadania z kolokwiów i egzaminów, zadania ze skryptu i własne formuły rozwiązujesz samodzielnie. Podpowiedzi zakładają, że dowodzona formuła jest prawem rachunku kwantyfikatorów — nie szukają kontrprzykładów.

Rezolucja (rozdz. 2.7)

• Zadanie: rozstrzygnij, czy zbiór klauzul jest sprzeczny. Jeśli tak — wyprowadź klauzulę pustą ⊥ (rezolucyjny dowód sprzeczności, Def. 47); jeśli nie — wskaż wartościowanie σ, które spełnia wszystkie klauzule.
• Kliknij dwie klauzule: dolny pasek pokaże ich rezolwenty — po jednej dla każdej zmiennej p, która w jednej klauzuli występuje jako p, a w drugiej jako ¬p. Kliknięta rezolwenta trafia na koniec listy. Gdy pojawi się ⊥, pod listą zobaczysz drzewo dowodu (jak na str. 43) i ciąg C₀, …, C_n.
• Wartościowanie ustawiasz w panelu po lewej (T albo F przy każdej zmiennej); przy klauzulach widać, czy są spełnione.
• Klauzule wpisuj jak w skrypcie: {¬p ∨ q, p, ¬q} albo ~p | q, p, ~q. Klauzule p ∨ q i q ∨ p (oraz p ∨ p i p) to ta sama klauzula.
• Zaznaczoną rezolwentę usuniesz klawiszem Delete (razem z rezolwentami, które z niej powstały); Ctrl+Z cofa ostatnią zmianę.
• Podpowiedzi (H) działają tylko w zbiorach przykładowych na górze menu Przykłady — z kolokwiów i egzaminów, do których opublikowano rozwiązania. Pozostałe zbiory z kolokwiów, egzaminów i ze skryptu rozwiązujesz samodzielnie.

Dwa tryby

• ↑ Od celu. Dodaj cel, kliknij go i wybierz regułę. Nad celem pojawią się przesłanki, a dla (⇒i), (¬i) i (∨e) — okna z założeniami. Powtarzaj, aż nie zostanie żaden otwarty cel.
• ↓ Od przesłanek. Dodaj przesłanki (hipotezy), zaznacz formuły na dole fragmentów i wybierz regułę — pod spodem pojawi się wniosek. Kolejność kliknięć ma znaczenie, np. dla (∧i) i (∨e). Reguły z oknem zamykają w nim wszystkie hipotezy równe założeniu.
• Tryby można łączyć: gotowy fragment wstawisz w otwarty cel z tą samą formułą (Wstaw fragment w cel), a poddrzewo możesz odłączyć jako osobny fragment.

Założenia są lokalne

• Z założenia wolno korzystać wyłącznie wewnątrz jego okna — tylko tam działa reguła założenie.
• Otwarte cele to po prostu niezamknięte hipotezy. W trybie „od przesłanek” nagłówek fragmentu pokazuje sekwent Γ ⊢ φ, gdzie Γ to te hipotezy. Dowód jest kompletny, gdy Γ jest puste — wtedy nagłówek pokazuje ⊢ φ.

Wnioski z założeń

• Kliknij założenie w nagłówku okna i wybierz regułę na dolnym pasku — pod założeniem pojawi się wniosek. Np. z p ∧ q regułami (∧e₁) i (∧e₂) dostaniesz p oraz q.
• Z wniosków można wyciągać kolejne: kliknij jeden albo dwa (np. p i p ⇒ q dla (⇒e)). Działają reguły eliminacji oraz (∧i) i (∨i); wolno łączyć założenia okna z założeniami okien, które je otaczają.
• Wnioski działają jak założenia: cel w tym oknie równy wnioskowi zamyka się sam (albo regułą założenie), a do dowodu trafia pełne wyprowadzenie — np. (∧e₁) nad założeniem. Zaznaczony wniosek usuniesz klawiszem Delete.

Cofanie kroków

• Cofnij krok (Delete): zaznacz uzasadnioną formułę albo kliknij nazwę reguły przy kresce — reguła zostanie cofnięta, a formuła znów będzie otwartym celem. Kroki wykonane nad przesłankami nie giną: zostają jako osobne fragmenty, które wstawisz z powrotem (zaznacz otwarty cel i wybierz Wstaw fragment w cel) albo usuniesz. Przy zaznaczonym otwartym celu cofa się krok, z którego ten cel powstał.
• Cofnij całe poddrzewo (Shift+Delete) usuwa wszystko nad formułą. Gdy najedziesz na któryś z tych przycisków, rysunek pokaże, co zostanie cofnięte.
• W trybie „od przesłanek” cofnięcie kroku na dole fragmentu rozdziela go z powrotem na przesłanki.
• Przycisk ↶ na górze (Ctrl+Z) cofa ostatnią zmianę, jakakolwiek by była — także cofnięcie kroku; ↷ (Ctrl+Y) ją przywraca.

Gotowy dowód

• Pod kompletnym dowodem pojawia się dowód w języku naturalnym — rozumowanie na wartościowaniach, jak w rozdz. 2 skryptu: dla dowolnego wartościowania σ pokazuje, że σ̂(φ) = T, a okna stają się przypadkami (wcięte akapity). Nazwy reguł można dopisać przełącznikiem, a całość skopiować jako zwykły tekst albo kod LaTeX.
• Odtwórz (skrót P) pokazuje dowód krok po kroku w trybie prezentacji z dużą czcionką — „od celu” albo „od przesłanek”. Strzałkami przechodzisz między krokami, a F włącza pełny ekran.
• Eksport zapisuje dowód jako obrazek PNG lub SVG (np. do notatek albo na Discorda — Kopiuj PNG i wklej) albo jako kod LaTeX.

Wpisywanie formuł

• Klikaj symbole w kreatorze albo pisz: ~ ! - → ¬, & /\ → ∧, | \/ → ∨, -> => → ⇒, T 1 → ⊤, F 0 → ⊥ (w rachunku kwantyfikatorów tylko T, F — cyfry są tam stałymi).
• Najsilniej wiąże ¬, potem ∧, ∨ i ⇒; ∧ i ∨ są łączne lewostronnie, a ⇒ — prawostronnie (np. p ⇒ q ⇒ r to p ⇒ (q ⇒ r)).

Skróty

• Shift/Ctrl/⌘ + klik — dodaj do zaznaczenia (w trybie „od przesłanek” wystarczy zwykłe kliknięcie).
• N następny otwarty cel · H podpowiedź · P prezentacja · Delete cofnij krok · Shift+Delete cofnij całe poddrzewo · Esc odznacz · Ctrl+Z / Ctrl+Y cofnij / ponów.

Podpowiedzi

• Podpowiedzi działają tylko w zadaniach przykładowych na górze menu Przykłady — to zadania z kolokwiów, do których opublikowano rozwiązania. Pozostałe zadania z kolokwiów i egzaminów, zadania ze skryptu i własne formuły rozwiązujesz samodzielnie.
• Przycisk Podpowiedź działa dla zaznaczonego celu, a gdy nic nie jest zaznaczone — dla następnego otwartego celu.
• Kolejne naciśnięcia odsłaniają coraz więcej: 1. wskazówka, od czego zacząć; 2. konkretna reguła z parametrem (pulsuje na pasku i w tabeli); 3. wykonanie tego kroku.
• Jeśli cel w danym miejscu nie wynika z dostępnych założeń, podpowiedź pokaże kontrprzykład (wartościowanie) i wskaże krok, w którym dowód zabrnął w ślepy zaułek — można go cofnąć jednym kliknięciem.

Zapis i udostępnianie

• Praca zapisuje się automatycznie w tej przeglądarce. Przycisk z łańcuchem kopiuje link zawierający cały dowód.
• Przełącznik Białe / Czarne w nagłówku zmienia tło aplikacji; wybór jest zapamiętywany (domyślnie tło jest białe).