Тысячи задач для средств доказательства теорем - Википедия - Thousands of Problems for Theorem Provers

TPTP (Тысячи задач для доказательства теорем)[1] это свободно доступный сборник задач для автоматическое доказательство теорем. Он используется для оценки эффективности автоматизированных алгоритмов рассуждения.[2][3][4] Проблемы выражаются в простом текстовом формате для логики первого или более высокого порядка.[5] TPTP используется как источник некоторых проблем в CASC.

Рекомендации

  1. ^ «Библиотека задач TPTP для автоматизированного доказательства теорем».
  2. ^ Ходер, Крыштоф; Воронков, Андрей (2009). «Сравнение алгоритмов объединения при доказательстве теорем первого порядка». CiteSeerX  10.1.1.329.1809. Дои:10.1007/978-3-642-04617-9_55. Цитировать журнал требует | журнал = (помощь)
  3. ^ Херд, Джо (2003). "Тактика доказательства первого порядка в средствах доказательства логических теорем высокого порядка". Цитировать журнал требует | журнал = (помощь)
  4. ^ Сегре, Альберто Мария; Стерджилл, Дэвид Б. (1994). «Использование сотен рабочих станций для решения логических задач первого порядка» (PDF). AAAI-94 Протоколы.
  5. ^ Бенцмюллер, Кристоф; Рабе, Флориан; Сатклифф, Джефф (2008). «THF0 - Ядро языка TPTP для логики высшего порядка». Дои:10.1007/978-3-540-71070-7_41. Цитировать журнал требует | журнал = (помощь)

внешняя ссылка