Мне нужен рабочий учебник по Isabelle и Sledgehammer

Question

Я установил последний пакет Isabelle/jEdit на свой компьютер с Windows. Я использовал официальный пакет с сайта Isabelle. Затем я открыл учебники, которые находятся на веб-странице Isabelle, и я начал компьютерные эксперименты. Я сразу понял, что многие примеры, представленные в этих учебниках, просто не работают в моей установке! К примеру, в этом tutorial на странице 5 следующий очень простой пример программы Isabelle представлена:

theory Test imports Main begin 
lemma "[a]=[b] ⟹ a=b" 
sledgehammer 

Ничто из этого не работал в моей установке!

1. Изабель жаловалась, что формула «[а] ═ [Ь] ⟹ а = Ь» имеет внутреннюю лексической ошибка: «Не удалось разобрать проп»

2. Когда я заменил эту формулу, работая один «(A & B) ⟹ «Команда« кувалда »не сработала. Я получил сообщение в поле целей

   цели (1 подцель)

   1. (A & B ⟹ A) & & & кувалды

вместо применения этой странной кувалды. Попытка назвать этот кувалдой кнопкой jEdit также не удалась, я получил сообщение об ошибке «Отсутствие функции печати« кувалда »»

Итак, мой вопрос сообществу. Есть ли какое-нибудь учебное пособие Изабель с кувалдой, последней версией? Или, по крайней мере, набор примеров РАБОТЫ на начальном уровне.

Answer 1

Оба примера работают без каких-либо проблем с моей установкой Isabelle 2015 (и я должен быть очень удивлен, если бы это было на Isabelle 2014 или 2013).

Причина Isabelle дает лексическую ошибку на [a]═[b] ⟹ a=b является то, что первым знаком равенства в этой формуле не знака равенства, но мальчик рисования характера. Я понятия не имею, как вам удалось найти этого персонажа, но если вы замените его знаком равенства, он будет работать.

Во втором примере кажется, что как-то «кувалда» анализировался как термин, а не как команда. Я понятия не имею, как это может быть (особенно не без видя точный код, введенный), но следующие прекрасно работает на моей установке:

theory Scratch 
imports Main 
begin 

lemma "(A & B) ⟹ A" 
sledgehammer 

EDIT: Ах, я не смог увидеть, что вы используете Изабеллу для Окна. У меня нет опыта работы с Isabelle для Windows, но я бы предположил, что в вашем случае есть проблема с Sledgehammer и Isabelle на Windows. Если пример, который я напечатал ранее, не работает с вашей установкой, я предлагаю вам написать электронное письмо в список рассылки и сообщить о проблеме, потому что он абсолютно должен работать.

В любом случае, из того, что я слышал, Isabelle в Windows несколько болезненна, и в идеале следует использовать Linux или Mac OS.

С другой стороны, Кувалда отнюдь не Существенный Компонент Изабель. Вы можете легко использовать и изучать Изабель без Кувалды. В качестве учебника я могу порекомендовать книгу Concrete Semantics. (Бесплатно PDF версия)

Answer 2

Обновление: Добавлен скриншот и связанный с ним ссылку на список пользователя Изабеллы.

Цель примера в учебнике Sledgehammer - убедиться, что ваша установка работает. Проблема в том, что ваша установка не работает, а не то, что учебник не «РАБОТАЕТ».

Я скопировал и вставил следующее:

lemma "[a]=[b] ⟹ a=b" 
sledgehammer 

Он работает.

Я использую Sledgehammer в течение более 3 лет в Windows 7. Он работает сейчас. Это сработало для меня с самого начала. Я только что начал с Isabelle2015, но то, что я показываю ниже, показывает, что все нормально.

я вставил в этом:

lemma "(A & B) ⟹ A" sledgehammer 

Он работает. Она возвращает

Try this: by simp (0.0 ms) 

для z3, spass, cvc4, e, remote_vampire и remote_e_sine.

Это тайна для меня, почему люди говорят, что Кувалда не работает на Windows. Я предполагаю, что это их антивирус. Я использую Norton, и он время от времени закрывает установку Isabelle и даже polyml, но никогда не является кузнецами.

Однако Sledgehammer запускает внешние ATP-преобразователи: z3, spass, cvc4 и e, поэтому не будет удивлять, что антивирус отключает их.

Не верь мне, Верь глазам

Вот скриншот:

проблема Мартини с Sledgehammer на Windows,

Особым бразильском с доктором философии в компьютере у науки возникли проблемы с тем, что Sledgehammer не работает в Windows.

Вот ссылка на потоки 2015-май: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-May/thread.html.

Искать по "Alfio Martini" в своем браузере, чтобы узнать, что он может сказать в разных сообщениях. Он начинает здесь: Re: [isabelle] Isabelle2015-RC3 available for testing.

(Примечание: Это не идеальный пример его проблем с сообщением с Кувалдой. В другом посте, возможно, в мае он говорил о том, что Кувалда не работает вообще.)

Сообщения о проблемах, связанных с кандидатом на выпуск, могут быть труднодостижимы, поскольку многочисленные проблемы публикуются под одним и тем же названием.

В основном, он говорит, что Кувалда никогда не работал на него в Windows. Это противоположность моему опыту. Кувалда всегда работала для меня в разумных пределах, то есть при нормальных «ошибках» современного программного обеспечения.

В разных сообщениях к списку он говорит несколько вещей, например, что он использует Windows 8.1. Похоже, что у него было несколько антивирусных программ, один из которых был «старым».

В результате получается, что он запустил его, но никогда не объяснял подробно, что он сделал, чтобы заставить его работать.

Он упомянул о нескольких проблемах с кувалдой, что я уверен, что не имеет никакого отношения к тому, что «Кувалда не работает вообще», например проблемы, связанные с cvc4.

Если Sledgehammer никогда не не возвращается к простой лемме, как он описывает, существует серьезная проблема, которая должна быть решена с помощью установки.

У меня никогда не было серьезной проблемы с Кувалдой на Windows 7. У меня был Norton, выключенный poly.exe и не уведомив меня об этом, что вызвало у меня много горя, пока я не понял.