Loading AI tools
Z Wikipedii, wolnej encyklopedii
Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli jest programem, a jest formułą, to wyrażenie postaci jest formułą algorytmiczną. W ten sposób mamy do czynienia ze splotem dwu algebr: algebry Boole’a i algebry programów. Znaczenie formuły jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu i znaczenie formuły Przypomnijmy, że znaczeniem formuły (pierwszego rzędu) jest funkcja ze zbioru wartościowań zmiennych w zbiór {true, false} wartości logicznych. Znaczeniem programu jest funkcja (częściowa) ze zbioru wartościowań w ten sam zbiór. Teraz znaczenie formuły możemy opisać w następujący sposób: dla danego wartościowania zmiennych należy najpierw wyznaczyć wynik obliczenia programu i z kolei obliczyć wartość formuły dla wartościowania W przypadku gdy obliczenie programu dla wartościowania nie daje wyniku, przyjmujemy, że wartością formuły jest false.
W języku logiki algorytmicznej można wyrażać semantyczne własności programów. Aksjomaty i reguły wnioskowania AL pozwalają na dowodzenie prawdziwych (semantycznie) formuł algorytmicznych. Oznacza to, że uzyskujemy możliwość dowodzenia faktów postaci: ten program jest poprawny względem warunku początkowego i warunku końcowego Formuła taka ma postać implikacji
Język określa się, podając jego alfabet i zbiór wyrażeń poprawnie zbudowanych WFF. W zbiorze wyrażeń poprawnie zbudowanych wyróżniamy trzy podzbiory: zbiór termów (albo zbiór wyrażeń nazwowych), zbiór formuł (zbiór wyrażeń logicznych) i zbiór programów (algorytmów).
Język logiki algorytmicznej jest konwolucją języka logiki pierwszego rzędu i języka programów.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.