Alle Optionen
stretch  ] [  buster  ] [  bullseye  ] [  bookworm  ] [  sid  ]
[ Quellcode: alt-ergo  ]

Paket: alt-ergo (1.30-1)

Links für alt-ergo

Screenshot

Debian-Ressourcen:

Quellcode-Paket alt-ergo herunterladen:

Betreuer:

Externe Ressourcen:

Ähnliche Pakete:

Automatischer Theorembeweiser zur Programmverifikation

Alt-Ergo ist ein automatischer Theorembeweiser, ausgerichtet auf die Anwendung zur Programmverifikation. Er basiert auf CC(X), einem Kongruenzabschluss-Algorithmus parametrisiert durch eine Gleichungstheorie X. Alt-Ergo verfügt über eingebaute Beweiser für Aussagenlogik, lineare Arithmetik, uninterpretierte Funktionssymbole, assoziativ-kommutative Funktionssymbole, polymorphe Arrays, benutzerdefinierte polymorphe Record-Typen und polymorphe Aufzählungstypen. Er bietet eingeschränkte Unterstützung für die Argumentation über beliebige benutzerdefinierte algebraische Typen, Quantoren erster Ordnung und nichtlineare Arithmetik.

Dieses Paket enthält den Beweiser als Befehlszeilenwerkzeug und als Version mit grafischer Oberfläche.

Markierungen: Implementiert in: OCaml, Rolle: Programm, GUI-Baukasten: GTK

Andere Pakete mit Bezug zu alt-ergo

  • hängt ab von
  • empfiehlt
  • schlägt vor
  • erweitert

alt-ergo herunterladen

Download für alle verfügbaren Architekturen
Architektur Paketgröße Größe (installiert) Dateien
amd64 2.318,0 kB13.637,0 kB [Liste der Dateien]
arm64 2.346,2 kB13.544,0 kB [Liste der Dateien]
armel 2.209,2 kB11.602,0 kB [Liste der Dateien]
armhf 2.280,8 kB9.650,0 kB [Liste der Dateien]
i386 2.102,0 kB11.818,0 kB [Liste der Dateien]
mips 325,5 kB3.445,0 kB [Liste der Dateien]
mips64el 325,4 kB3.445,0 kB [Liste der Dateien]
mipsel 325,3 kB3.445,0 kB [Liste der Dateien]
ppc64el 325,4 kB3.445,0 kB [Liste der Dateien]
s390x 325,4 kB3.445,0 kB [Liste der Dateien]