Изабель 2017 начало работы

Я пытаюсь научиться использовать Isabelle / HOL. Я подумал: «Эй, учебник, написанный некоторыми людьми, которые его разработали, было бы здорово», и поэтому посмотрел на https://isabelle.in.tum.de/doc/tutorial.pdf, дата публикации которого - 15 августа 2018 г. Однако, пытаясь проработать примеры, я нахожу кое-что вот так в тексте:

«Классический пользовательский интерфейс Isabelle - это Proof General / Emacs Дэвида Аспиналла. В этой книге очень мало говорится о Proof General, у которой есть собственная документация». (страница iii)

«Если произойдет что-нибудь странное, мы рекомендуем вам попросить Изабель отобразить всю информацию о типе через пункт меню Proof General Isabelle> Настройки> Показать типы (подробности см. В разделе 1.5)». (стр. 5)

Проблема в том, что Proof General, похоже, больше не работает с Isabelle (см. Isabelle2016 и Proof General) . Я не понимаю, почему учебное пособие основано на устаревшем программном обеспечении, но на самом деле мой вопрос таков:

«Есть ли где-нибудь, где я могу научиться делать даже самые простые вещи в Isabelle 2017?»


theorem-proving isabelle
person John    schedule 13.12.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

По состоянию на 2018 год единственной IDE, поддерживаемой для Isabelle, является Isabelle / jEdit, которая включена в дистрибутив, который вы можете загрузить с веб-сайта Isabelle. Существует экспериментальный плагин VSCode, который находится в стадии активной разработки, но я бы рекомендовал пока использовать Isabelle / jEdit.

Найденное вами руководство указано на веб-сайте как одно из «старых руководств». Он во многих отношениях сильно устарел, и его больше не следует использовать. Дата публикации, вероятно, не имеет смысла, поскольку это дата создания PDF-файла, а не дата написания текста. Некоторые люди лоббировали полное удаление этого руководства с веб-сайта, и ваш опыт, похоже, подтверждает, что мы действительно должны это сделать.

Один из лучших способов начать изучение Изабель - это, вероятно, книга «Конкретная семантика» (бесплатная онлайн-версия доступный). Его первая половина - это, по сути, введение в Isabelle / HOL с большим количеством упражнений. Также имеется руководство по «Программирование и испытание». на сайте Изабель, что почти идентично первой половине «Конкретной семантики».

Однако он ориентирован на приложения в области информатики (семантика языков программирования и немного функционального программирования). Я не уверен, есть ли хороший учебник о том, как заниматься математикой в ​​Изабель; в любом случае, математику, как правило, труднее выполнять в программе доказательства теорем для новичков, потому что разрыв с неформальными бумажными рассуждениями больше. Поэтому я рекомендую «Конкретную семантику», даже если вы в конечном итоге заинтересованы в формализации математики.

Кстати: вы упомянули Isabelle2017, но на самом деле нет причин использовать это вместо Isabelle2018, которая является самой последней версией на момент написания этого ответа.

person Manuel Eberl    schedule 13.12.2018
comment
Я должен доверять группе людей, которые не могут отличить дату авторства от даты создания pdf, как людям, которые скажут мне, правильно ли программное обеспечение? :) Так или иначе, спасибо за указатель. Я спросил о 2017 году, потому что с этой версией я работал, когда в последний раз это меня настолько расстроило, что я сдался. (Вздох.) - person John; 13.12.2018
comment
На dream.inf ЕСТЬ довольно хороший учебник по математике в Isabelle. ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf ... но, к сожалению, он привязан к Proof General (хотя я уверен, что опытный пользователь мог бы это прочитать). - person John; 13.12.2018
comment
В самом деле, вы можете просто игнорировать все ссылки на Proof General. Это не сильно меняет. Однако точные названия некоторых теорем / определений понятий могут иногда немного изменяться между выпусками Isabelle. Кроме того, этот учебник по математике охватывает только довольно простые вещи; Чтобы делать «настоящие» математические доказательства в isabelle, очень полезно иметь опыт работы с доказательствами Isar и умением использовать автоматизацию. Более того, использование таких вещей, как пределы и интегралы, требует некоторого привыкания. - person Manuel Eberl; 14.12.2018
comment
К счастью, моя цель состоит в том, чтобы сделать некоторые доказательства в синтетической проективной геометрии, так что ничего ужасно фантастического - конечно, не более причудливого, чем та часть теории групп, которая хорошо документирована, например, на веб-сайте Изабель. Но, как вы отметили, некоторое понимание Isar и автоматизации явно полезно даже в этом случае. - person John; 14.12.2018