Translate answer set programs to first-order theorem prover language
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.ci
app
examples
include/anthem
lib
src
tests
.gitattributes
.gitmodules
.travis.yml
CHANGELOG.md
CMakeLists.txt
LICENSE.md
README.md

README.md

anthem GitHub Release Build Status Build Status

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

$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...

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 requires CMake for building. After installing the dependencies, anthem is built with a C++17 compiler (GCC ≥ 7.3 or clang ≥ 5.0).

$ git clone https://github.com/potassco/anthem.git
$ cd anthem
$ git submodule update --init --recursive
$ mkdir -p build/release
$ cd build/release
$ cmake ../.. -DCMAKE_BUILD_TYPE=Release
$ make

Contributors