Ich suche nach einem Werkzeug (GUI bevorzugt, aber CLI würde funktionieren), das es mir erlaubt, mathematische Ausdrücke einzugeben und sie dann zu manipulieren, aber mich nur auf mathematisch gültige Operationen beschränkt. Außerdem muss das Tool in der Lage sein, eine Sitzung zu speichern und später zu beweisen, dass die angegebene Gruppe gespeicherter Operationen gültig ist.
Hinweis: Ich bin Nicht suche nach einem System, Proofs zu generieren, nur dass die von mir manuell angegebenen Schritte gültig sind.
Ich habe ACL2 für ähnliche Operationen verwendet, und es funktioniert in einigen Fällen gut, aber es ist sehr schwer für alles zu verwenden sonst.
Dieses kleine Projekt ist meine Motivation. Es ist ein D-Schablonentyp, der eine Gleichung ermöglicht lösen. Angesichts dieser Gleichung:
%Vor%Jedes der Symbole kann als unbekannt festgelegt werden, und die Auswertung dieses Ausdrucks führt zu einer Zuweisung zu dieser Variablen. Es funktioniert, indem man Ausdrucksbäume in den Typ einbaut und dann mit Umschreibungsregeln in etwas umwandelt, das für den unbekannten Typ ausgeführt werden kann.
Was ich brauche, ist eine Möglichkeit, die Rewrite-Regel zu validieren. Sie können validiert werden, indem man die Behauptung prüft, dass eine gegebene Beziehung wahr ist, eine andere auch.
ACL2 ist berüchtigt - wir sagten immer, es sei ein Expertensystem und könne daher nur von Experten benutzt werden, die von Warren Hunt, J Moore oder Bob Boyer lernen mussten. Was Sie in ACL2 tun müssen, ist wirklich wirklich zu verstehen, wie das Proof-System selbst funktioniert. dann können Sie es in Richtungen anzeigen, die den Suchraum verkleinern.
Es gibt verschiedene andere Systeme, die bei dieser Art von Problemen helfen können, je nachdem, was Sie versuchen.
Wenn Sie mit kontinuierlicher Mathematik oder Zahlentheorie arbeiten möchten, ist das Ideal
Etwas ähnliches und kostenloses ist Open Maxima , was eine Erweiterung von Macsyma ist. Diese Seite weist auch auf einige andere wie Axiom hin, mit denen ich keine Erfahrung habe.
Für Operationen mit mathematischer Logik gibt es PVS von SRI. Sie haben einige andere coole Sachen wie Model-Checking im selben Rahmen.
Mehrere amerikanische Beweisassistenten wurden bereits erwähnt (normalerweise mit LISP-Syntax), daher gibt es hier eine europäische Liste, die diese ergänzt:
Alle sind berüchtigt für TTY-Schnittstellen, aber Coq und Isabelle bieten gute Unterstützung für die Proof General / Emacs-Schnittstelle. Darüber hinaus kommt Coq mit CoqIDE, das auf OCaml / GTK und dem integrierten Text-Widget basiert. Letzte Isabelle enthält die Isabelle / jEdit Prover-IDE, die auf jEdit basiert und durch semantisches Markup erweitert wird, das vom Prover in Echtzeit bereitgestellt wird, während der Benutzer tippt.
Es gibt in diesem Bereich laufende Forschung, es heißt "Theorem in der Computeralgebra".
Menschen versuchen, die Benutzerfreundlichkeit und Leistungsfähigkeit von Computeralgebra-Systemen wie Mathematica, Maple, ... mit der logischen Strenge von Proof-Systemen zu vereinen. Die Probleme sind:
Computeralgebrasysteme sind nicht streng. Sie neigen dazu, Seitenbedingungen zu vergessen, so dass ein Divisor nicht 0 sein darf.
Die Beweis-Systeme sind hart und langwierig zu benutzen (wie Sie entdeckt haben).
Tags und Links math coq theorem-proving isabelle proof-system