Logika Algorytmiczna: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 1: Linia 1:
Logika algorytmiczna jest rachunkiem logicznym. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. Zbiór formuł
+
Logika algorytmiczna jest rachunkiem logicznym. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Zadaniem logiki algorytmicznej jest poszukiwanie praw rachunku programów.
algorytmicznych zawiera w sobie zbiór formuł pierwszego rzedu.
+
 
 +
 
== Program logiki algorytmicznej ==
 
== Program logiki algorytmicznej ==
 
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc.
 
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc.

Wersja z 17:03, 28 kwi 2014

Logika algorytmiczna jest rachunkiem logicznym. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Zadaniem logiki algorytmicznej jest poszukiwanie praw rachunku programów.


Program logiki algorytmicznej

Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc. Znaczeniem programu [math]P[/math] jest funkcja ze zbioru [math]W[/math] wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję te określa sie przy pomocy pojęcia obliczenia programu.