Translate answer set programs to first-order theorem prover language (local mirror of https://github.com/potassco/anthem for development purposes)
https://potassco.org/
Patrick Lühne
ea885f5fdb
Clingo treats operations that were assumed to be “invalid” not as processing errors but as operations returning an empty set. This changes how formulas have to be evaluated. This commit implements an explicit function for retrieving the return type of an expression, that is, both the domain of the result as well as whether it’s an empty, unit, or general set with multiple values. |
||
|---|---|---|
| .ci | ||
| app | ||
| examples | ||
| include/anthem | ||
| lib | ||
| src | ||
| tests | ||
| .gitattributes | ||
| .gitmodules | ||
| .travis.yml | ||
| CHANGELOG.md | ||
| CMakeLists.txt | ||
| LICENSE.md | ||
| 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 [--complete] [--simplify] file...
--complete instructs anthem to perform Clark’s completion on the translated formulas.
With the option --simplify, the output formulas are simplified by applying several basic transformation rules.
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