W dniu piątek, 27 marca 2015 10:57:26 UTC+1 użytkownik g...@g...com napisał:
> > Myślę że w praktyce w ogóle nie ma możliwości przeprowadzenia takiego
> > dowodu, nawet dla mniejszych programów. Jak udowodnić, że w dowodzie
> > nie ma błędu?
>
> To jest akurat rzecz podstawowa: wystarczy pokazać, że każdy krok dowodu
> wynika logicznie z tez dowiedzionych wcześniej, albo przyjętych przez nas
> aksjomatów, w oparciu o uznawane przez nas reguły wnioskowania
> (które uważamy za oczywiste).
>

nie jestem pewien czy to wystarczy.. czasem moze nawet dosyc czesto moze okazac sie
ze
mio ze te wnioskowania byly poprawne to
ogolnie problem wynika z przeoczenia pewnych
pobocznych czynników

innymi slowy mi wyglada na to ze dowody sa
rowniez czesciowe tak samo jak testy ;/

> Walidacja dowodu jest zabiegiem bardzo prostym -- z pewnością
> o wiele prostszym, niż znalezienie dowodu.
>
> Oczywiście pewien problem natury epistemicznej wiąże się ze sformułowaniem
> odpowiedniej listy aksjomatów, które miałyby odzwierciedlać rozważany
> przez nas problem