zachjhansen / anthem-rs

🎼 Translate answer set programs to first-order theorem prover language

anthem

Translate answer set programs to first-order theorem prover language

Overview

anthem translates ASP programs (in the input language of clingo) to the language of first-order theorem provers such as Prover9.

Usage

To verify that a program implements a specification, invoke anthem using the verify-program command:

$ anthem verify-program <program file> <specification file>...

Note that multiple specification files may be specified. This is useful for separating lemmas and axioms from the assumptions and specs.

The example for computing the floor of the square root of a number can be reproduced as follows:

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

The braces notation is a Bash shorthand for

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

By default, anthem performs Clark’s completion on the translated formulas, detects which variables are integer, and simplifies the output by applying several basic transformation rules.

These processing steps can be turned off with the options --no-complete, --no-simplify, and --no-detect-integers.

Warnings can be shown by setting the environmental variable ANTHEM_LOG to "warn"

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

Building

anthem is built with Rust’s cargo toolchain. After installing Rust, anthem can be built as follows:

$ git clone https://github.com/potassco/anthem.git
$ cd anthem
$ cargo build --release

The anthem binary will then be available in the target/release/ directory. Alternatively, anthem can be invoked using cargo as follows:

$ cargo run -- verify-program <program file> <specification file>...

Contributors

• Patrick Lühne