anthem 1

hymne

Traduire les programmes d'ensembles de réponses en langage de preuve de théorème du premier ordre

Statut de ce projet

Note

Vous consultez actuellement la version 1 d' anthem , qui a été construite par Patrick Lühne et n'est plus en cours de développement. Aucun autre engagement dans ce référentiel ne sera effectué.

Si vous êtes intéressé par une version récente d'Anthem, jetez un œil au nouveau référentiel.

Aperçu

anthem traduit les programmes ASP (dans le langage d'entrée de clingo ) dans le langage des prouveurs de théorèmes du premier ordre tels que Prover9.

Usage

Pour vérifier qu'un programme implémente une spécification, invoquez anthem à l'aide de la commande verify-program :

 $ anthem verify-program <fichier programme> <fichier de spécification>...

Notez que plusieurs fichiers de spécifications peuvent être spécifiés. Ceci est utile pour séparer les lemmes et les axiomes des hypothèses et des spécifications.

L’exemple de calcul du plancher de la racine carrée d’un nombre peut être reproduit comme suit :

 $ anthem verify-program examples/example-2.{lp,spec,lemmas}

La notation par accolades est un raccourci Bash pour

 $ anthem verify-program examples/example-2.lp examples/example-2.spec exemples/example-2.lemmas

Par défaut, anthem effectue la complétion de Clark sur les formules traduites, détecte quelles variables sont entières et simplifie la sortie en appliquant plusieurs règles de transformation de base.

Ces étapes de traitement peuvent être désactivées avec les options --no-complete , --no-simplify et --no-detect-integers .

Bâtiment

anthem est construit avec la chaîne d'outils cargo de Rust. Après avoir installé Rust, anthem peut être construit comme suit :

 $ git clone https://github.com/potassoco/anthem.git
Hymne du CD $
$ cargo build --release

Le binaire anthem sera alors disponible dans le répertoire target/release/ . Alternativement, anthem peut être invoqué en utilisant cargo comme suit :

 $ cargo run -- verify-program <fichier programme> <fichier de spécification>...

Contributeurs

• Patrick Lühne