anthem

Translate answer set programs to first-order theorem prover language

Status of this project

Note

You’re currently looking at version 1 of anthem, which was built by Patrick Lühne and is no longer being developed. No further commits to this repository will be made.

If you're interested in a recent version of anthem, have a look at the new repository.

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.

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