BourbakiProving

система автоматической проверки доказательств из книги Бурбаки

Пока и 3й параграф 1й главы не реализован

todo

• переименовать contradiction в contr

• проверять already_exist на то, что из двух одинаковых утверждений может следоватьтолько одно

• сделать списки перебора

  • или порядок поиска утверждений по длине названия
  • или потом перевести весь поиск на дерево поиска

• доделать fast exist

  • вывод на печать и убрать повторную проверку.

• добавить 2 режима генерации tgf-файлов

• доказать все логические утверждения и прописать подсказки

• переходить к кванторным теориям