⊢

Dedukcja naturalna

rachunek zdań · dowody z oknami, jak w rozdz. 2.9 skryptu

Reguły

Automatycznie zamykaj cele, które są założeniami otaczającego okna

Przykłady

Podpowiedzi

Eksport do LaTeX-a

Kod używa pakietu proof (polecenie \infer) i makra \okno, które rysuje pudełko z założeniem. Kompiluje się pdflatex-em; dokument standalone daje przycięty obrazek dowodu.

pełny dokument (standalone)

Jak korzystać

φ otwarty cel / niezamknięta hipoteza φ zaznaczenie α założenie okno z założeniem

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 o tej samej formule (Wstaw fragment w cel), a poddrzewo możesz odłączyć jako osobny fragment.

Założenia są lokalne

Założenia wolno używać tylko wewnątrz jego okna — reguła założenie jest dostępna tylko tam.
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 ⊢ φ.

Wpisywanie formuł

Klikaj symbole w kreatorze albo pisz: ~ ! - → ¬, & /\ → ∧, | \/ → ∨, -> => → ⇒, T 1 → ⊤, F 0 → ⊥.
Kolejność wiązania: ¬, ∧, ∨, ⇒; ∧ i ∨ łączą w lewo, ⇒ w prawo (np. p ⇒ q ⇒ r to p ⇒ (q ⇒ r)).

Skróty

Shift/Ctrl/⌘ + klik — dodaj do zaznaczenia (w trybie „od przesłanek” każdy klik dodaje).
N następny otwarty cel · Delete usuń uzasadnienie · Esc odznacz · Ctrl+Z / Ctrl+Y cofnij / ponów.

Podpowiedzi

Przycisk Podpowiedź (skrót H) 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 skręcił 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. Bez wyboru obowiązuje ustawienie systemu.