Jape: Графический помощник для доказательства теорем в математической логике.
Jape (software)
Jape – графический помощник для доказательства теорем, разработанный для обучения математической логике. Бесплатная программа на Java для Mac, Unix, Windows.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Jape — это настраиваемый графический помощник для доказательств, изначально разработанный Ричардом Борнатом в Университете Королевы Марии в Лондоне и Бернардом Суфрином в Оксфордском университете. Программа доступна для операционных систем Mac, Unix и Windows. Она написана на языке программирования Java и распространяется под лицензией GNU GPL. Утверждается, что Jape является самой популярной программой для обучения логике с использованием компьютера, включающего упражнения по построению доказательств в математической логике.
Jape is a configurable, graphical proof assistant, originally developed by Richard Bornat at Queen Mary, University of London and Bernard Sufrin the University of Oxford. The program is available for the Mac, Unix, and Windows operating systems. It is written in the Java programming language and released under the GNU GPL. It is claimed that Jape is the most popular program for "computer assisted logic teaching" that involves exercises in developing proofs in mathematical logic.
История
Jape был создан в 1992 году Ричардом Борнатом и Бернардом Суфрином с целью более глубокого понимания формального мышления. Бернард Суфрин предложил название "Jape". В 2019 году они опубликовали код на GitHub.
Jape was created in 1992 by Richard Bornat and Bernard Sufrin with the intent to get a better understanding of the formal reasoning. Bernard Sufrin came up with the name "Jape". In 2019, they released the code on GitHub.
Обзор
Jape поддерживает направленное пользователем построение доказательств в логике, определяемой пользователем как система правил вывода. Он сопоставляет жесты пользователя (например, ввод текста, щелчки или перетаскивание мышью) с действиями ассистента при построении доказательства. Jape не обладает специальными знаниями о какой-либо конкретной логике или теории и выполняет шаги в доказательстве только в том случае, если они обоснованы правилами текущей загруженной логики. Jape позволяет выполнять шаги доказательства и отменять их, а также отображает эффект добавленных шагов, что помогает понять стратегии поиска доказательств. По мере добавления и удаления шагов доказательства строится дерево доказательства, которое Jape может отображать в виде дерева или в блочной форме. Jape позволяет отображать доказательства на различных уровнях абстракции. Также возможно представить прямое доказательство в стиле естественной дедукции, используя специализированные режимы отображения. Jape работает с вариантами исчисления секвенций и естественной дедукции, а также поддерживает формальные доказательства с кванторами.
Jape supports human directed discovery of proofs in a logic which is defined by the user as a system of inference rules. It maps the user's gestures (e. g. typing, mouse clicks or mouse drags) to the assistant's proof actions. Jape does not have any special knowledge of any object logic or theory, and it will make moves in a proof if and only if they are justifiable by rules of the object logic that is currently loaded. Jape allows to make proof steps and undo them, and it shows the effect of the added proof steps which helps to understand strategies for finding proofs. When the user adds and removes the proof steps, the proof tree is constructed which Jape can show either in a tree shape or in box forms. Jape allows to display proofs at different levels of abstraction. It is also possible to present a forward proof in a natural deduction style by using the specialized modes of display for proofs. Jape works with variants of the sequent calculus and natural deduction. It also supports formal proofs with quantifiers.