Привести любую формулу на языке предикатов 1го порядка к СКНФ (C# / Prolog).

[emppu2007]

Всем привет.
Тема моей расчётно-графической работы по ИИ была "Автодоказательство теорем". Там всё было несложно, описал процедуру конъюнкции, импликации, логического отрицания, дальше разбил задачу на рассмотрение 6 правил вывода и, собственно, исходя из них, теорема и доказывалась.
Препод дал дополнительное задание на автомат: привести любую формулу на языке предикатов 1го порядка к СКНФ.
Теоретически, похоже на мою расчётку.
Нужно (наверное о_О) только добавить несколько процедур и вывод изменить.
Но категорически не успеваю, т.к. диплом пишу.
Экзамен уже 14.06, а на него идти я не хочу. Хочу автомат))
Читал Братко - в нём ни слова про СКНФ/КНФ и всё остальное.
Исходников тоже не могу никаких найти.
Пишите, кто в состоянии помочь.
Договоримся о цене.
Кому нужно - могу скинуть свою РГР. Возможно, её будет легче переделать под эту тему. И дешевле.

P.S. Вообще, решить задачу нужно на SWI/Turbo Prolog'e, но на C# тоже можно.