anthem 1

himno

Traducir programas de conjuntos de respuestas al lenguaje de demostración de teoremas de primer orden

Estado de este proyecto

Nota

Actualmente estás viendo la versión 1 de anthem , que fue creada por Patrick Lühne y ya no se está desarrollando. No se realizarán más compromisos con este repositorio.

Si estás interesado en una versión reciente de Anthem, echa un vistazo al nuevo repositorio.

Descripción general

anthem traduce programas ASP (en el lenguaje de entrada clingo ) al lenguaje de demostradores de teoremas de primer orden como Prover9.

Uso

Para verificar que un programa implemente una especificación, invoque anthem usando el comando verify-program :

 $ himno verificar-programa <archivo de programa> <archivo de especificación>...

Tenga en cuenta que se pueden especificar varios archivos de especificaciones. Esto es útil para separar lemas y axiomas de los supuestos y especificaciones.

El ejemplo para calcular el suelo de la raíz cuadrada de un número se puede reproducir de la siguiente manera:

 $ ejemplos de programas de verificación de himno/ejemplo-2.{lp,spec,lemas}

La notación de llaves es una abreviatura de Bash para

 $ ejemplos de programa de verificación de himno/ejemplo-2.lp ejemplos/ejemplo-2.spec ejemplos/ejemplo-2.lemmas

De forma predeterminada, anthem realiza la finalización de Clark en las fórmulas traducidas, detecta qué variables son enteras y simplifica la salida aplicando varias reglas de transformación básicas.

Estos pasos de procesamiento se pueden desactivar con las opciones --no-complete , --no-simplify y --no-detect-integers .

Edificio

anthem está construido con la cadena de herramientas cargo de Rust. Después de instalar Rust, anthem se puede construir de la siguiente manera:

 $ git clon https://github.com/potassco/anthem.git
$ cd himno
$ construcción de carga --liberación

El binario anthem estará disponible en el directorio target/release/ . Alternativamente, se puede invocar anthem usando cargo de la siguiente manera:

 $ ejecución de carga --verificar-programa <archivo de programa> <archivo de especificación>...

Colaboradores

• Patricio Lühne