anthem 1

гимн

Перевести программы набора ответов на язык доказательства теорем первого порядка.

Статус этого проекта

Примечание

В настоящее время вы просматриваете первую версию anthem , созданную Патриком Люне и больше не разрабатываемую. Никаких дальнейших коммитов в этот репозиторий делаться не будет.

Если вас интересует последняя версия Anthem, загляните в новый репозиторий.

Обзор

anthem переводит программы ASP (на входном языке clingo ) на язык средств доказательства теорем первого порядка, таких как Prover9.

Использование

Чтобы убедиться, что программа реализует спецификацию, вызовите anthem с помощью команды verify-program :

 $ anthemverify-program <файл программы> <файл спецификации>...

Обратите внимание, что можно указать несколько файлов спецификации. Это полезно для отделения лемм и аксиом от предположений и спецификаций.

Пример вычисления нижнего квадратного корня числа можно воспроизвести следующим образом:

 $ anthem проверки-программы примеры/пример-2.{lp,spec,lemmas}

Обозначение фигурных скобок — это сокращение Bash для

 $ anthem проверки-программы примеры/пример-2.lp примеры/пример-2.спец примеры/пример-2.леммы

По умолчанию anthem выполняет автодополнение Кларка для переведенных формул, определяет, какие переменные являются целочисленными, и упрощает вывод, применяя несколько основных правил преобразования.

Эти этапы обработки можно отключить с помощью опций --no-complete , --no-simplify и --no-detect-integers .

Здание

anthem создан с использованием cargo инструментария Rust. После установки Rust anthem можно собрать следующим образом:

 $ git клон https://github.com/potassco/anthem.git
$ компакт-диск с гимном
$грузовая сборка --выпуск

После этого двоичный файл anthem будет доступен в каталоге target/release/ . В качестве альтернативы, anthem можно вызвать с помощью cargo следующим образом:

 $ Cargo Run --verify-program <файл программы> <файл спецификации>...

Авторы

• Патрик Люне