Большинство помощников по доказательству - это функциональные языки программирования с зависимыми типами. Они могут проверять программы / алгоритмы. Вместо этого меня интересует помощник по доказательству, который лучше всего подходит для математики и только (например, для исчисления). Вы можете порекомендовать один? Я слышал о Mizar, но мне не нравится, что исходный код закрыт, но если это лучше для математики, я воспользуюсь им. Насколько хорошо новые языки, такие как Agda и Idris, подходят для математических доказательств?
Помощник по доказательству только по математике
comment
Какие!? исходный код для Mizar закрыт ?!
- person Charlie Parker schedule 28.11.2018
Ответы (1)
Coq имеет обширные библиотеки, охватывающие реальный анализ. На ум приходят разные разработки:
стандартная библиотека и основанные на ней проекты, такие как ныне несуществующий coqtail [1] (с обширным охватом степенных рядов и довольно небольшой работой над комплексными числами) или более поздний проект coquelicot. Все они основаны на аксиоматическом определении реальных объектов, представленном здесь.
Более конструктивный подход обеспечивается проектом C-CoRN, который начинается с фактического построения реалов.
Еще один способ разобраться с реальностью - обратиться к нестандартному анализу. Именно этим занимаются люди, использующие ACL2.
Чтобы получить более общее представление о поле, вам, вероятно, следует прочитать этот обзорный доклад людей, участвующих в проекте coquelicot.
[1] полное раскрытие: я участвовал в этом проекте
person
gallais
schedule
16.02.2015
Могу ли я предположить из вашего ответа, что Agda не подходит для математических доказательств?
- person M.K.; 11.01.2016
Вся моя работа (в интерфейсе программирования и тестирования) за последние 4 года была сделана в Agda. И есть довольно большие проекты формализации, полностью выполненные в Agda. Но Coq извлекает выгоду из большой работы, направленной на автоматизацию некоторых надоедливых доказательств (например, всех (не) равенств при работе с кольцами, полями и т. Д.). В конце концов, ответ будет зависеть от того, какой математикой вы хотите заниматься.
- person gallais; 11.01.2016
Есть ли преимущества от использования Mizar?
- person Charlie Parker; 28.11.2018
