Было бы разрешено - не было бы треда. Только логика L, только хардкор (т.е., доказывать только через стандартные 3 аксиомы, теорему дедукции и ее следствия, также можно использовать 10 классических теорем).
Есть много програмок по доказательству теорем вроде E http://www4.informatik.tu-muenchen.de/~schulz/E/E.html, но они в нагрузку еще обычно используют более сложные правила с целью оптимизации. Для простого набора правил и простой формулы думаю можно самому попробовать написать, думаю строк 100 кода получится.