Delta 4/2017 Twierdzenie o niepustym barze, czyli zmechanizowana naturalna dedukcja Jacek Chrząszcz informatyka