Question  |
Answer |
|
start learning
|
|
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? start learning
|
|
|
|
|
Czy intuicjonistyczny rachunek zdań jest rozstrzygalny? start learning
|
|
|
|
|
Czy rachunek predykatów jest rozstrzygalny start learning
|
|
|
|
|
Co to rachunek predykatów? start learning
|
|
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)
|
|
|
|
start learning
|
|
zdania służace za punkty wyjscia w dochodzeniu do wniosku
|
|
|
|
start learning
|
|
składa się z przesłanek oraz wniosku, w sekwencie możliwe jest udowodnienie wniosku za pomocą przesłanek
|
|
|
Czym jest zdanie atomowe? start learning
|
|
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? start learning
|
|
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 start learning
|
|
przez kwantyfikator x jest zmienna zwiazana a y zmienna wolna
|
|
|
logiki temporalne LTL i CTL czym sie róznia? start learning
|
|
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
|
|
|
|
start learning
|
|
{P} C{Q} - jeżeli p jest spelnione przed wykonaniem c (instrukcji) dojdzie do Q
|
|
|
|
start learning
|
|
ϕ1, ..., ϕn |= ψ oznacza jeśli w pewnym wartościowaniu wszystkie formuły ϕi mają znaczenie T to i ψ ma znaczenie T
|
|
|
|
start learning
|
|
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ł
|
|
|
|
start learning
|
|
o narzędzie i język służący do budowania i analizy modeli systemów
|
|
|
|
start learning
|
|
zbiór symboli i reguł jak je ze sobą łączyć.
|
|
|
|
start learning
|
|
nadanie symbolom znaczenia. np funkcjonalnosc tabelki prawdy
|
|
|
|
start learning
|
|
jezeli zdanie w danym systemie jest prawdziwe, istnieje dowód który potrafi to udowodnić
|
|
|
Podaj 3 systemy pełne i 1 niezupełny start learning
|
|
rachunek zdań klasyczny, intuicjonistyczny i rachunek poredykatów. Logika w połaczeniu z arytmetyką jest NIEZUPEŁNA
|
|
|
Czemu rachunek predykatow jest nierozstrzygalny? start learning
|
|
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)
|
|
|
|
start learning
|
|
Formuła jest spełnialna, jeśli istnieje przynajmniej jedno wartościowanie dla którego formuła jest Prawdziwa
|
|
|
|
start learning
|
|
Program, który automatycznie sprawdza, czy formuła jest spełnialna (zamiast sprawdzać całą tabelkę prawdy).
|
|
|
Czym jest zalozenie pragmatyczne start learning
|
|
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 start learning
|
|
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
|
|
|
