• Artykuły
  • Forum
  • Ciekawostki
  • Encyklopedia
  • Automatyczne dowodzenie twierdzeń

    Przeczytaj także...
    Rachunek zdań – dział logiki matematycznej badający związki między zmiennymi zdaniowymi (zdaniami) lub funkcjami zdaniowymi, utworzonymi za pomocą funktorów zdaniotwórczych (spójników zdaniowych) ze zdań lub prostszych funkcji zdaniowych. Rachunek zdań określa sposoby stosowania funktorów zdaniotwórczych w poprawnym wnioskowaniu.Komputer (z ang. computer od łac. computare – liczyć, sumować; dawne nazwy używane w Polsce: mózg elektronowy, elektroniczna maszyna cyfrowa, maszyna matematyczna) – maszyna elektroniczna przeznaczona do przetwarzania informacji, które da się zapisać w formie ciągu cyfr albo sygnału ciągłego.
    Rozstrzygalność (decydowalność) problemu matematycznego to następująca jego właściwość: istnieje algorytm, który oblicza odpowiedź na dowolne pytanie stawiane przez problem.

    Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) – proces, w którym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiejś teorii, często przy okazji generując jego dowód. Twierdzenia te należą zwykle do rachunku zdań lub rachunku predykatów pierwszego rzędu.

    System wspomagający dowodzenie twierdzeń (ang. prover) – program komputerowy pozwalający użytkownikowi na zapis wyrażeń i formuł matematycznych oraz pomagający przy przeprowadzaniu ich dowodu. W ogólności automatyczne dowodzenie twierdzeń jest niemożliwe, gdyż dla wielu logik pytanie, czy dana formuła ma dowód jest nierozstrzygalne, dlatego provery zazwyczaj tylko asystują użytkownikowi przy przeprowadzaniu dowodu i weryfikują, czy użytkownik nie wykonuje niedozwolonych operacji. Zwykle potrafią również znaleźć dowody dla prostych faktów lub udzielić użytkownikowi wskazówek, które drogi rozumowania mogą doprowadzić do wyniku, niemniej ich moc jest mocno ograniczona.Równość – relacja, która jest relacją równoważności. Jest to zatem relacja zwrotna, przechodnia i symetryczna. Ważną cechą relacji równości a = b {displaystyle a=b} jest to, że dla dowolnej funkcji f {displaystyle f} zachodzi:

    Dla komputera wygodniejsze jest zwykle wnioskowanie w tył, choć czasem stosuje się też wnioskowanie w przód.

    Automatyczne dowodzenie twierdzeń rachunku zdań[]

    Chodzi o stwierdzenie czy dane twierdzenie jest tautologią, lub czy jest spełnialne. Oba przypadki są wzajemnie połączone: zaprzeczenie twierdzenia jest spełnialne wtedy i tylko wtedy, gdy twierdzenie to nie jest tautologią.

    Twierdzenia rachunku zdań zawsze są rozstrzygalne – choćby metodą brute force, która polega na sprawdzeniu 2 kombinacji wartości prawda-fałsz dla n zmiennych zdaniowych występujących w twierdzeniu.

    Alfred Tarski wł. Alfred Tajtelbaum (ur. 14 stycznia 1901 w Warszawie, zm. 26 października 1983 w Berkeley, Kalifornia, USA) – polski logik pracujący od 1939 r. w Stanach Zjednoczonych. Twórca m.in. teorii modeli i semantycznej definicji prawdy, uważany jest współcześnie za jednego z najwybitniejszych logików wszech czasów.Rezolucja to metoda automatycznego dowodzenia twierdzeń oparta na generowaniu nowych klauzul, aż dojdzie się do sprzeczności. W ten sposób można udowodnić, że dane twierdzenie nie jest spełnialne, lub też, co jest równoważne, że jego zaprzeczenie jest tautologią.

    Istnieje wiele innych metod, które mają większą wydajność i generują bardziej czytelne dowody. Do najprostszych z nich należą sekwenty Gentzena, systemy Hilberta oraz dedukcja naturalna. W praktyce używa się zwykle metod bazowanych na procedurze Davisa-Putnama. Można też używać uproszczonych wersji metod dla rachunku predykatów pierwszego rzędu.

    Procedura Davisa-Putnama – bardzo efektywny system dowodzenia twierdzeń dla rachunku zdań. Istnieją też jego modyfikacje dla rachunku predykatów pierwszego rzędu, jednak są one zwykle mniej wydajne od rezolucji.Algorytm siłowy, algorytm brute force (ang. "brutalna siła" tj. niewspomagana umysłem) – określenie algorytmu, który opiera się na sukcesywnym sprawdzeniu wszystkich możliwych kombinacji w poszukiwaniu rozwiązania problemu, zamiast skupiać się na jego szczegółowej analizie.

    Problem spełnialności jest jednak w każdym systemie NP zupełny, zaś problem tautologii – CoNP zupełny.

    Automatyczne dowodzenie twierdzeń rachunku predykatów[]

    Dominujące metody to tableau, a przede wszystkim różne wersje rezolucji. W systemach z równością używa się też paramodulacji. Warto zaznaczyć, że "ogólny" język I rzędu jest nierozstrzygalny. W szczególności nie istnieje algorytm, który dla ogólnego języka I rzędu może określić, czy dane zdanie jest w nim prawdziwe, czy nie. Istnieją jednak "szczególne" języki I rzędu, które są rozstrzygalne. Przykładem rozstrzygalnego języka I rzędu może być arytmetyka liczb rzeczywistych, co udowodnił Alfred Tarski. Do weryfikacji zdań o liczbach rzeczywistych służy metoda eliminacji kwantyfikatorów.

    System Hilberta – dowolny system automatycznego dowodzenia twierdzeń, w którym występuje pewien zbiór aksjomatów i reguł dowodzenia, a dowód składa się z ciągu formuł będących albo aksjomatami, albo formułami wyprowadzonymi z poprzednich formuł na podstawie reguł dowodzenia, z których ostatnia jest właśnie formułą którą chcemy dowieść. Jest to wnioskowanie w przód w przeciwieństwie do wnioskowania w tył znanego z innych systemów dowodzenia.Problemy Co-NP-zupełne to takie problemy klasy Co-NP, że każdy inny problem klasy Co-NP może zostać do nich zredukowany, analogicznie jak dla problemów NP-zupełnych. Ponadto problem dopełniający względem problemu NP-zupełnego jest NP-trudny.

    Zobacz też[]

  • rachunek lambda
  • CADE
  • CASC
  • subsumpcja
  • unifikacja
  • term
  • indeksowanie termów
  • system wspomagający dowodzenie twierdzeń
  • system Mizar



  • w oparciu o Wikipedię (licencja GFDL, CC-BY-SA 3.0, autorzy, historia, edycja)

    Warto wiedzieć że... beta

    Wnioskowanie w przód (Modus Ponendo Ponens) – progresywny algorytm sztucznej inteligencji służący do tworzenia nowych zdań logicznych na podstawie istniejącej bazy faktów, aksjomatów.
    Unifikacja (ang. unification) to operacja na dwóch lub więcej drzewach, która znajduje takie przyporządkowanie zmiennych, że drzewa te są równe. Np. (w notacji lispowej): (+ x 2) i (+ (+ z 7) y) są unifikowalne dla y=2 i x=(+ z 7). (+ x 2) i (+ y 3) nie są unifikowalne. Podobnie unifikowalne nie są (* x 2) i (+ x x) ani (+ 2 3) i (+ 3 2) - unifikacja dotyczy tylko symboli nie ich znaczenia.
    Rachunek predykatów pierwszego rzędu – (ang. first order predicate calculus) to system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu "dla każdej funkcji z X na Y ..." (gdyż funkcja jest podzbiorem X × Y), "istnieje własność p, taka że ..." czy "dla każdego podzbioru X zbioru Z ...". Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną).
    Sekwenty Gentzena – jeden z najprostszych sposobów automatycznego dowodzenia twierdzeń rachunku zdań. Został opracowany przed Gerharda Gentzena w 1934 roku. Znany jest również pod nazwą system LK od niemieckiej nazwy Logischer Kalkül. Jest to jednocześnie jedna z formalizacji rachunku predykatów.
    W logice matematycznej teorią nazywamy niesprzeczny zbiór zdań. Dokładniej, niech T będzie zbiorem zdań zapisanych w pewnym języku L. Wtedy T jest teorią, jeśli nie istnieje zdanie napisane w języku L takie że T dowodzi zarówno tego zdania, jak i jego zaprzeczenia. Zbiór zdań T dowodzi zdania X, jeśli można przeprowadzić formalny dowód zdania X przy użyciu zdań ze zbioru T oraz aksjomatów i reguł dowodzenia klasycznego rachunku logicznego.
    Zbiór liczb rzeczywistych – uzupełnienie zbioru liczb wymiernych. Zbiór liczb rzeczywistych zawiera m.in. liczby naturalne, ujemne, całkowite, pierwiastki liczb dodatnich, wymierne, niewymierne, przestępne, itd. Z drugiej strony na liczby rzeczywiste można też patrzeć jak na szczególne przypadki liczb zespolonych.
    Zmienna zdaniowa – bezargumentowy symbol w rachunku zdań. Zmiennym zdaniowym, w procesie zwanym wartościowaniem, przyporządkowywane są wartości prawda lub fałsz.

    Reklama

    Czas generowania strony: 0.05 sek.