Тысячи задач для доказывающих теоремы

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

TPTP (Thousands of Problems for Theorem Provers) ^[1] — это свободно доступная коллекция задач для автоматизированного доказательства теорем . Она используется для оценки эффективности алгоритмов автоматизированного рассуждения. ^{[2] [3] [4]} Задачи выражены в простом текстовом формате для логики первого порядка или логики высшего порядка. ^[5] TPTP используется в качестве источника некоторых задач в CASC .

Ссылки

1. «Библиотека задач TPTP для автоматического доказательства теорем».
2. Hoder, Kryštof; Voronkov, Andrei (2009). "Сравнение алгоритмов объединения в доказательстве теорем первого порядка". KI 2009: Достижения в области искусственного интеллекта . Конспект лекций по информатике. Том 5803. С. 435–443. CiteSeerX 10.1.1.329.1809 . doi :10.1007/978-3-642-04617-9_55. ISBN  978-3-642-04616-2.
3. Херд, Джо (2003). «Тактика доказательства первого порядка в средствах доказательства теорем логики высшего порядка». S2CID  11201048. {{cite journal}}: Цитировать журнал требует |journal=( помощь )
4. Сегре, Альберто Мария; Стерджил, Дэвид Б. (1994). «Использование сотен рабочих станций для решения логических задач первого порядка» (PDF) . Труды AAAI-94 .
5. Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff (2008). "THF0 – The Core of the TPTP Language for Higher-Order Logic". Автоматизированное рассуждение . Конспект лекций по информатике. Том 5195. С. 491–506. doi :10.1007/978-3-540-71070-7_41. ISBN 978-3-540-71069-1.

Внешние ссылки

• Официальный сайт