Автоматическое Доказательство теорем - Prolog

Формулировка задачи:

извините, я сам заочник, у меня курсовая горит тема размытая, связанная с автоматическим доказательством теорем, программа на прологе главная задача, нужно доказательство одной-двух любой теоремы реализуемое на прологе, кучу книг читаю, вот Братко есть, но там сложно как то, мне бы программу с коментариями вообщем программа нужна на прологе которая доказывает любую математическую теорему, однако из дискретки будет проще написать, вот беда пролог мало чего в нем знаю, да и как это вообще сделать тож на форуме только сегодня, впервые такое просто помогите пожалуйста с этим, может есть на форуме что то такое, или может сделать кто поможет_?( или может кто такое делал уже //если из а следует b и из b следует с, то из а следует с //(а => b) & (b => с) => (а => с) вот, однако что то такое попробовать или может что нить другое_?( вот читаю щас это через резолюцию доказывают, а как на прологе сделать_?(

Решение задачи: «Автоматическое Доказательство теорем»

textual
                            Листинг программы 
                        

                            /*
  con(impl(var('s'),no(var('t'))),var('t'))
  reduce(con(impl(var('s'),no(var('t'))),var('t')),T,0).
  */
                        