Посоветуйте систему автоматического доказательства теорем

На логике первого порядка. Только не prolog.

Ссылка

← Повторная обработка результата запроса

Mono GTK# vs. PyGTK Что православней и больше доставляет? →

На Лиспе пишется за пару вечеров.

anonymous
(21.02.14 14:34:50 MSK)

хацкель?
чем пролог то не устроил? просто и понятный язык

TERRANZ ★★★★
(21.02.14 14:39:55 MSK)
Последнее исправление: TERRANZ 21.02.14 14:40:11 MSK (всего исправлений: 1)

~~baverman~~ ★★★
(21.02.14 14:40:57 MSK)

Ссылка

Ответ на: комментарий от TERRANZ 21.02.14 14:39:55 MSK

Prolog - это урезанный FOL. Не подходит

nerdogeek ★
(21.02.14 14:45:17 MSK) автор топика
Последнее исправление: nerdogeek 21.02.14 14:45:29 MSK (всего исправлений: 1)

Ссылка

Coq? Agda? что такое логика первого порядка я не знаю.

Dark_SavanT ★★★★★
(21.02.14 16:32:25 MSK)

Ответ на: комментарий от Dark_SavanT 21.02.14 16:32:25 MSK

С синтаксисом максимально схожим с логикой предикатов. Просто не верю что такого нет.
Вот что-то подобное, но оно глючноватое и урезанное

nerdogeek ★
(21.02.14 16:54:43 MSK) автор топика

Ссылка

аспирантота

geek ★★★
(21.02.14 16:56:50 MSK)

Ссылка

Любой SMT-солвер. Например, Z3. http://rise4fun.com/Z3

(граждане, советующие кок и агду для автоматического доказательства, одновременно не зная про first-order logic — лор во всей красе)

mkmks
(21.02.14 20:47:36 MSK)