Дайте (программное обеспечение)
| Оригинальный автор(ы) | Ричард Борнат , Бернар Сюфрин |
|---|---|
| Стабильная версия | 9.1.8 [1]
/ 10 октября 2023 г |
| Репозиторий | github |
| Написано в | OCaml , Java |
| Тип | Помощник по доказательствам |
| Лицензия | Лицензия GPL-2.0 |
Jape — это настраиваемый помощник по графическому доказательству , первоначально разработанный Ричардом Борнатом из Лондонского университета Королевы Марии и Бернардом Суфрином университета из Оксфордского . [2] Программа доступна для операционных систем Mac , Unix и Windows . Он написан на языке программирования Java и выпущен под лицензией GNU GPL .
Утверждается, что Jape — самая популярная программа для «обучения логике с помощью компьютера», которая включает в себя упражнения по разработке доказательств математической логики . [3]
История
[ редактировать ]Jape был создан в 1992 году Ричардом Борнатом и Бернаром Суфрином с целью лучше понять формальные рассуждения. Бернар Суфрин придумал название «Джейп». [2]
В 2019 году они опубликовали код на GitHub. [4]
Обзор
[ редактировать ]под руководством человека Jape поддерживает обнаружение доказательств в логике, которая определяется пользователем как система правил вывода . Он сопоставляет жесты пользователя (например, ввод текста, щелчки мышью или перетаскивание мыши) с проверочными действиями помощника. Jape не обладает какими-либо специальными знаниями о какой-либо объектной логике или теории , и он будет делать ходы в доказательстве тогда и только тогда, когда они оправданы правилами объектной логики, которая в данный момент загружена. [5] Jape позволяет выполнять шаги доказательства и отменять их, а также показывает эффект добавленных шагов доказательства, что помогает понять стратегии поиска доказательств. [2] : 60 Когда пользователь добавляет и удаляет этапы доказательства, строится дерево доказательства, которое Jape может отображать либо в виде дерева, либо в виде прямоугольников. [5] Jape позволяет отображать доказательства на разных уровнях абстракции. Также возможно представить прямое доказательство в стиле естественной дедукции, используя специальные режимы отображения доказательств. [6]
Джейп работает с вариантами секвенциального исчисления и естественной дедукции . Он также поддерживает формальные доказательства с помощью кванторов . [2] : 84
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ «Исправленное завершение доказательства (и фиксированные окна защиты от зомби)» . Гитхаб . Проверено 11 января 2024 г.
- ^ Jump up to: а б с д Борнат, Ричард (1 февраля 2017 г.). «Доказательство и опровержение в формальной логике: введение для программистов» (PDF) . Архивировано (PDF) из оригинала 18 апреля 2022 г. Проверено 11 января 2024 г.
- ^ Цезарь Калишик; Фрик Видейк; Максим Хендрикс; Фемке ван Раамсдонк (2007). «Преподавание логики с использованием современного помощника по доказательству» (PDF) . Х. Геверс и П. Куртье (ред.), PATE'07, Международный семинар по помощникам и типам доказательств в образовании : 37–50. Архивировано из оригинала (PDF) 17 января 2023 года.
- ^ «(Измененный) первый выпуск GitHub» . Гитхаб . 6 декабря 2019 года . Проверено 11 января 2024 г.
- ^ Jump up to: а б Суфрин, Бернар; Борнат, Ричард (3 апреля 1998 г.). «Пользовательские интерфейсы для универсальных помощников по проверке. Часть I: Интерпретация жестов» (PDF) . Архивировано (PDF) из оригинала 15 августа 2023 г. Проверено 11 января 2024 г.
- ^ Суфрин, Бернар; Борнат, Ричард (март 1998 г.). «Пользовательские интерфейсы для универсальных помощников по проверке доказательств. Часть II: Отображение доказательств» (PDF) . Архивировано (PDF) из оригинала 11 января 2024 г. Проверено 11 января 2024 г.
Внешние ссылки
[ редактировать ]- Jape Online Официальный сайт распространения
- Jape SourceForge Портал
- Джейп на Github