Интерактивная математическая система

Question

Я ищу инструмент (предпочтительнее GUI, но CLI будет работать), который позволяет мне вводить математические выражения и затем манипулировать ими, но ограничивает меня только математически допустимыми операциями. Кроме того, инструмент должен быть в состоянии сохранить сеанс, а затем доказать, что данный набор сохраненных операций действителен.

Примечание. Я Не ищу систему для генерации подтверждений, только для проверки правильности указанных вручную шагов.

Я использовал ACL2 для аналогичных операций, и он хорошо работает в некоторых случаях, но его очень трудно использовать для всего остального.

Этот небольшой проект является моей мотивацией. Это тип шаблона D, который позволяет решать уравнения. Учитывая это уравнение:

(A * B) = C + D / F;

Любой из символов может быть установлен как неизвестный, и оценка этого выражения приведет к присвоению этой переменной. Он работает, встраивая деревья выражений в тип, а затем используя правила перезаписи, чтобы преобразовать его во что-то, что можно определить для неизвестного типа.

Мне нужен какой-то способ проверки правила перезаписи. Их можно проверить, проверив утверждение, что если какое-то отношение истинно, другое также.

Answer 1

Несколько американских помощников по проверке уже упоминались (обычно с синтаксисом LISP), поэтому вот европейский список, дополняющий это:

• Coq

• Isabelle

• HOL4

• HOL-Light

• Мицар

Все они известны своими интерфейсами TTY, но Coq и Isabelle обеспечивают хорошую поддержку интерфейса Proof General / Emacs. Кроме того, Coq поставляется с CoqIDE, который основан на OCaml / GTK и встроенном текстовом виджете. Последняя версия Isabelle включает IDE Isabelle / jEdit Prover, которая основана на jEdit и дополнена семантической разметкой, предоставляемой проверяющим в режиме реального времени при вводе пользователем.

Answer 2

ACL2 печально известен - мы привыкли говорить, что это была экспертная система, и поэтому ее могли использовать только эксперты, которые должны были учиться у Уоррена Ханта, Дж. Мура или Боба Бойера. В ACL2 вам нужно по-настоящему понять, как работает сама система проверки; тогда вы можете «намекнуть» на это в направлениях, которые уменьшают пространство поиска.

Есть несколько других систем, которые могут помочь с этим, хотя, в зависимости от того, что вы пытаетесь сделать.

Если вы хотите работать с непрерывной математикой или теорией чисел, идеал будет Mathematica . Проблема в том, что вы можете купить подержанный автомобиль за ту же сумму (если вы не можете претендовать на академическую лицензию, гораздо выгоднее).

Нечто похожее и бесплатное - Open Maxima , которое является расширением Macsyma. Эта страница также указывает на несколько других, таких как Аксиома, с которыми у меня нет опыта.

Для математических логических операций есть PVS от SRI. У них есть другие интересные вещи, такие как проверка моделей в той же самой структуре.

Answer 3

В этой области продолжаются исследования, которые называются «Доказательство теорем в компьютерной алгебре».

Люди пытаются объединить простоту использования и мощь систем компьютерной алгебры, таких как Mathematica, Maple, ... с логической строгостью систем доказательств. Проблемы:

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

• Системы доказательства трудны и утомительны в использовании (как вы обнаружили).

Answer 4

Бережливый прувер является интерактивным через графический интерфейс JS.

Answer 5

В дополнение к ссылкам Чарли Мартина, вы также можете проверить Клен . Мой опыт работы с таким программным обеспечением составляет около 5 лет, но я вспоминаю, что в то время Maple был гораздо более интуитивным, чем Mathematica.

Answer 6

Старая и не обслуживаемая система «Ontic»:

http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html