anthem 1

Hymne

Übersetzen Sie Antwortsatzprogramme in die Sprache des Theorembeweisers erster Ordnung

Status dieses Projekts

Notiz

Sie sehen sich derzeit Version 1 von anthem an, die von Patrick Lühne erstellt wurde und nicht mehr weiterentwickelt wird. Es werden keine weiteren Commits für dieses Repository vorgenommen.

Wenn Sie an einer aktuellen Version von Anthem interessiert sind, schauen Sie sich das neue Repository an.

Überblick

anthem übersetzt ASP-Programme (in der Eingabesprache clingo ) in die Sprache von Theorembeweisern erster Ordnung wie Prover9.

Verwendung

Um zu überprüfen, ob ein Programm eine Spezifikation implementiert, rufen Sie anthem mit dem Befehl verify-program auf:

 $ anthem verify-program <Programmdatei> <Spezifikationsdatei>...

Beachten Sie, dass mehrere Spezifikationsdateien angegeben werden können. Dies ist nützlich, um Lemmata und Axiome von den Annahmen und Spezifikationen zu trennen.

Das Beispiel zur Berechnung des Bodens der Quadratwurzel einer Zahl kann wie folgt wiedergegeben werden:

 $ Anthem Verify-Program-Beispiele/Beispiel-2.{lp,spec,lemmas}

Die Klammerschreibweise ist eine Bash-Abkürzung für

 $ Anthem Verifizierungsprogramm Beispiele/Beispiel-2.lp Beispiele/Beispiel-2.spec Beispiele/Beispiel-2.lemmas

Standardmäßig führt anthem die Clark-Vervollständigung der übersetzten Formeln durch, erkennt, welche Variablen ganzzahlig sind, und vereinfacht die Ausgabe durch die Anwendung mehrerer grundlegender Transformationsregeln.

Diese Verarbeitungsschritte können mit den Optionen --no-complete , --no-simplify und --no-detect-integers ausgeschaltet werden.

Gebäude

anthem wurde mit cargo -Toolchain von Rust erstellt. Nach der Installation von Rust kann anthem wie folgt erstellt werden:

 $ Git-Klon https://github.com/potassco/anthem.git
$ CD-Hymne
$ Cargo Build --Release

Die anthem Binärdatei ist dann im Verzeichnis target/release/ verfügbar. Alternativ kann anthem auch mit cargo wie folgt aufgerufen werden:

 $ cargo run -- verify-program <Programmdatei> <Spezifikationsdatei>...

Mitwirkende

• Patrick Lühne