Automated First Order Natural Deduction. - Alexander Bolotov; Vyacheslav Bocharov; Alexander Gorchakov; Vasilyi Shangin (IICAI, 2005)