Theorem proving software systems

Maple ist eine Umgebung für symbolisches und numerisches Rechnen sowie eine Programmiersprache mit mehreren Paradigmen .

Nqthm ist ein Theorembeweiser, der manchmal auch als Boyer-Moore-Theorembeweiser bezeichnet wird . Er war ein Vorläufer von ACL2 .

OBJ ist eine Programmiersprachenfamilie, die 1976 von Joseph Goguen eingeführt und von Jose Meseguer weiterentwickelt wurde .

Peter Bruce Andrews (1. November 1937 – 21. April 2025) war ein US-amerikanischer mathematischer Logiker. Er ist der Schöpfer der mathematischen Logik Q₀ .

Planner (in Publikationen oft als „PLANNER“ abgekürzt, obwohl es sich nicht um ein Akronym handelt) ist eine Programmiersprache, die von Carl Hewitt am MIT entwickelt und 1969 erstmals veröffentlicht wurde.

Wolfram Mathematica (auch bekannt als Mathematica ) ist ein Softwaresystem mit integrierten Bibliotheken für verschiedene Bereiche des technischen Rechnens.

Twelf ist eine Implementierung des logischen Frameworks LF, das von Frank Pfenning und Carsten Schürmann an der Carnegie Mellon University entwickelt wurde .