W powszechnie używanym paradygmacie programowania imperatywnego dowodzenie poprawności programów jest raczej trudne (np. metoda Hoare'a). Celem seminarium jest pokazanie o ile te sprawy są prostsze w programowaniu w logice (logic programming).
Postaram się przedstawić temat wielostronnie: z punktu widzenia wyników i własności matematycznych, a także nieformalnie - jak programista myśli o programach. Mam nadzieję uzasadnić tezę, że w programowaniu w logice programowanie jest istotnie łatwiejsze niż w programowaniu imperatywnym.
Przedstawię głównie wyniki prac własnych. Ciekawe, że zagadnienia te były traktowane po macoszemu przez wiele lat rozwoju teorii programowania w logice.
Rozpoczniemy od krótkiego wprowadzenia "dla każdego" do programowania w logice.