Logika 2026

Rozstrzygalność

czy istnieje algorytm, który powie nam dla dowolnego zdania TAK (jest prawdziwe) lub NIE w skończonym czasie

Czy klasyczny rachunek zdań jest rozstrzygalny?

Tak

Czy intuicjonistyczny rachunek zdań jest rozstrzygalny?

Tak

Czy rachunek predykatów jest rozstrzygalny

Nie

Co to rachunek predykatów?

system logiczny, w którym w przeciwienstwie od rachunku zdan analizujemy strukture zdań atomowych i wyszczegolnia: Elementy (Alicja, jezyk Java) Predyakty (lubi sie uczyc, jest studentka) Kwantyfikatory (każdy, niektórzy)

czym sa przesłanki?

zdania służace za punkty wyjscia w dochodzeniu do wniosku

czym jest sekwent?

składa się z przesłanek oraz wniosku, w sekwencie możliwe jest udowodnienie wniosku za pomocą przesłanek

Czym jest zdanie atomowe?

To zdanie, które nie zawiera żadnych spójników logicznych (i, lub, jeśli, nie). Nie da się go podzielić na mniejsze zdania

Czym różni sie logika intuicjonistyczna od klasycznej?

logika intuicjonistyczna nie uznaje a) prawa wyłącznego środka b) eliminacji podwójnej negacji c) dowodu nie w prost

zmienna wolna a zmienna związana

przez kwantyfikator x jest zmienna zwiazana a y zmienna wolna

logiki temporalne LTL i CTL czym sie róznia?

w LTL - czas jest liniowy i opisujemy ściezki w logice CTL czas jest rozgałęziony. W praktyce logiki ctl poprzedone są kwantifykatorami A lub E. w LTL podczas sprawdzania formuł domyślnie przyjmuje się kwantifykator A

Trójki Hoare’a

{P} C{Q} - jeżeli p jest spelnione przed wykonaniem c (instrukcji) dojdzie do Q

Implikacja semantyczna

ϕ1, ..., ϕn |= ψ oznacza jeśli w pewnym wartościowaniu wszystkie formuły ϕi mają znaczenie T to i ψ ma znaczenie T

Twierdzenie o pełności

Jeśli ϕ1, ..., ϕn |= ψ, to ϕ1, ..., ϕn ⊢ ψ tzn. jeśli zachodzi implikacja semantyczna, to istnieje formalny wywód formuły ze zbioru przesłanek i reguł

Alloy

o narzędzie i język służący do budowania i analizy modeli systemów

Co to język?

zbiór symboli i reguł jak je ze sobą łączyć.

semantyka

nadanie symbolom znaczenia. np funkcjonalnosc tabelki prawdy

pełność

jezeli zdanie w danym systemie jest prawdziwe, istnieje dowód który potrafi to udowodnić

Podaj 3 systemy pełne i 1 niezupełny

rachunek zdań klasyczny, intuicjonistyczny i rachunek poredykatów. Logika w połaczeniu z arytmetyką jest NIEZUPEŁNA

Czemu rachunek predykatow jest nierozstrzygalny?

Na to pytanie odpowiada problem stopu Turinga. problem ten mowi ze nie istnieje żaden program, który potrafi wziac inny program i powiedziec a) ten kod sie zawiesi (fałsz) b) ten kod skonczy sie powodzeniem (prawda)

Spełnialność

Formuła jest spełnialna, jeśli istnieje przynajmniej jedno wartościowanie dla którego formuła jest Prawdziwa

SAT solver

Program, który automatycznie sprawdza, czy formuła jest spełnialna (zamiast sprawdzać całą tabelkę prawdy).

Czym jest zalozenie pragmatyczne

Zamiast sprawdzać system dla każdego rozmiaru, sprawdzamy go tylko w małym zakresie (Scope). Jeśli SAT Solver nic nie znajdzie w tym zakresie, zakładamy pragmatycznie, że system jest poprawny (choć nie jest to dowód matematyczny, a inżynierski)

Poprawność czesciowa i calkowita

Poprawność częściowa mówi o tym, że jesli program sie zatrzyma wynik bedzie poprawny. Poprawność całkowita z kolei mówi ze program sie zatrzyma oraz wynik bedzie poprawny