1 Systemy wspomagające dowodzenie twierdzeń
2 operatory logiczne NEGACJA KONIUNKCJA ALTERNATYWA IMPLIKACJA RÓWNOWAŻNOŚĆ ALTERNATYWA WYKLUCZAJĄCA NEGACJA ALTERNATYWY NEGACJA KONIUNKCJI
3 Gramatyka formalna G = < V, T, P, S > V – zbiór symboli terminalnych – skończony, niepusty zbiór symboli końcowych, z których budowane są słowa generowane przez gramatykę (zwany czasem alfabetem końcowym) T – zbiór symboli nieterminalnych – skończony, niepusty zbiór symboli pomocniczych P – lista produkcji – reguły gramatyki S – symbol startowy (aksjomat) – jest to wyróżniony symbol pomocniczy, z niego wyprowadzane są wszystkie generowane przez gramatykę G napisy
4 Symbole terminalne operatory logiczne i zmienne zdaniowe (atomy ) Poczatkowy symbol startowy (nieterminalny)
5 Interpretacje Wartościowanie – przypisuje każdemu atomowi formuły wartosć logiczną Interpretacja - wartość logiczna formuły przypisana danemu wartościowaniu Np. koniunkcja jest prawdziwa gdy oba atomy prawdziwe w przeciwnym przypadku jest fałszywa Formuły logicznie równoważne: mające przy tym samym wartościowaniu tę samą wartość logiczną
6 Formuły spełnialne i tautologieFormuła spełnialna – prawdziwa dla pewnej interpretacji Tautologia – prawdziwa dla każdej interpretacji
7 Procedury decyzyjne Niech U będzie zbiorem formuł Procedura decyzyjna dla zbioru U; Algorytm który dla dowolnej formuły kończy działanie z odpowiedzią TAK jeśli należy ona do U oraz z odpowiedzią NIE gdy nie należy ona do U. Np. Procedurą decyzyjną rozstrzygającą czy dana procedura jest spełnialna jest Metoda Tabel Semantycznych
8 Model zbioru formuł Niech będzie zbiorem formuł oraz A będzie formułą. Interpretację, dla której jednocześnie wszystkie formuły z U są prawdziwe nazywamy modelem zbioru formuł Jeśli dla każdego modelu zbioru formuł U formuła A jest prawdziwa to nazywamy ją logiczną konsekwencją U.
9 Systemy dowodzenia Dana formuła jest twierdzeniem danej teorii jeśli jest logiczną konsekwencją zbioru aksjomatów tej teorii. System dowodzenia – - zbiór aksjomatów -zbiór reguł dowodzenia Dowód formuły A – ciąg formuł prowadzących od aksjomatów do formuły A, zgodne z regułami dowodzenia tak, aby A była ostatnim elementem tego ciągu. Wówczas A nazywamy twierdzeniem danej teorii co zapisujemy |-A
10 Reguła dowodzenia Reguły dowodzenia zapisujemyPRZESŁANKI KONKLUZJE Jeśli U jest twierdzeniem teorii, to V jest twierdzeniem teorii
11 SYSTEM GENTZENOWSKI Literał – atom lub negacja atomu Dla literału p para literałów komplementarnych Aksjomatem jest zbiór dowolnych formuł zawierający literały komplementarne
12 Reguły dowodzenia systemu gontzenowskiego
13
14 System Hilbertowski Reguła dowodzenia (modus ponens)
15 Reguły pochodne Niech U będzie zbiorem formuł, A formułą Zapis oznacza że formuły ze zbioru U są założeniami w dowodzie formuły A Wykorzystując aksjomaty i regułę modus ponens Dowodzi się reguł pochodnych np. Reguła dedukcji:
16 System Hilbertowski jest poprawny (formuły które mają dowód są prawdziwe) System Hilbertowski jest pełny (formuły prawdziwe mają dowód) System Hilbertowski jest niesprzeczny (nie mają jednoczesnie dowodu formuły komplementarne)
17 Mizar Tekst mizarowy zwany artykułem tworzy się przy użyciu zwykłego edytora tekstowego
18
19 Taktyki dowodzenia Taktyka założeniowa teza w postaci implikacji2. Taktyka adjunkcji Teza w postaci koniunkcji (trzeba udowodnić każdy z członów koniunkcji)
20 3. Taktyka generalizacji – teza z kwantyfikatorem ogólnym 43. Taktyka generalizacji – teza z kwantyfikatorem ogólnym 4. Taktyka egemplifikacji Teza z kwantyfikatorem szczegółowym
21 Pisząc tekst matematyczny pewne fakty uznajemy za prawdziwe (aksjomaty)
22 Niech dany będzie przedykat NW[a,b] - a nie wieksze niż b w dziedzinie ułamków
23 Przykład dowodu „nie wprost”