Translate answer set programs to first-order theorem prover language (local mirror of https://github.com/potassco/anthem for development purposes)
https://potassco.org/
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Patrick Lühne
e0aa3497ee
|
4 years ago | |
|---|---|---|
| .ci | 4 years ago | |
| app | 4 years ago | |
| examples | 4 years ago | |
| include/anthem | 4 years ago | |
| lib | 4 years ago | |
| src | 4 years ago | |
| tests | 4 years ago | |
| .gitattributes | 6 years ago | |
| .gitmodules | 4 years ago | |
| .travis.yml | 4 years ago | |
| CHANGELOG.md | 4 years ago | |
| CMakeLists.txt | 4 years ago | |
| LICENSE.md | 4 years ago | |
| README.md | 4 years ago | |
README.md
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
$ 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