Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Category:

Пруверство для дебилов

Нашёл, наконец, доказыватель теорем (Prover9 + Mace4), в котором у меня получается писать теории несмотря на своё тотальное невежество в этом вопросе. Для пользования CoQ или AGDA2 мне не хватало знаний соответствующих теорий типов. А здесь достаточно голой неконструктивной логики первого порядка (Prover4 всегда доказывает от противного). А может, просто руки прямее стали с тех времён, когда я в последний раз осторожно трогал Агду2 длинной палкой.

Ещё интересно наличие опровергателя Mace4. Он ищет для теорий Prover9 конечные модели, что можно использовать для отладки теории в процессе написания:

1) для доказательства непротиворечивости теории (если для теории существует модель - то теория непротиворечива)
2) для опровержения некоей теоремы контрпримером (если существует модель, в которой теорема не выполняется - то теорема ложна)
3) для доказательства назависимости некоей аксиомы (если модели существуют как теории с аксиомой, так и для теории с отрицанием этой аксиомы - то данная аксиома независима от остальных)
4) для иллюстрации в виде таблиц того, что за теорию вы пишете - в процессе написания оказывается, что есть неожиданные модели, которые нужно запрещать добавлением новых аксиом.
5) как подкрепление к Prover9 - можно запускать параллельно доказыватель и опровергатель и если один остановится - то второй можно убивать

В самообразовательных целях я, разумеется, пишу формальную теорию жопы, состоящую из "арифметики с самым большим числом" (где жопа возникает при переполнении) и "списков с максимальной длиной" (где жопа возникает при слишком длинных списках или при Head(Nil)).

Был бы признателен за литературу по разрешимым и-или конечным "арифметикам", которые "похожи" на "настоящую". Например, одни товарищи якобы обрезали разрешимую арифметику Пресбургера и получили разрешимость за экспоненциальное время, что в области пруверства является невероятно хорошим результатом (в "обычном" случае сложность алгоритма доказателсьства - некая "башня экспонент").
Tags: fp, programming
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 98 comments