Completor is a system for computing answer sets of normal logic programs with variables using finite model builders. It transforms the logic program to a first-order formula suitable for model builders. Completor can complete a logic program, clausify the completed theory and eliminate the introduced Skolem functions. The resulting formula is in the EPR class. It accepts the input program in a subset of Lparse's language and generates the output formula in TPTP format. In the experiments Paradox, iProver, and FM-Darwin and are used as finite model builders.
Completor is implemented by Orkunt Sabuncu. For your questions and comments please send an email to orkunt@ceng.metu.edu.tr.
The basic usage is
completor.py -clausify Defnoskolem input.lp > out.tptpIf there are constant variables in the input, you can assign values using the -c cons=val option. When using FM-Darwin, numbers in the input can be a problem. Use the -rn option to rename the numbers (for example object 0 becomes n_0)
Generate a clausal theory (without Skolem functions) and assign 50 to p and h:
completor.py -c p=50 -c h=50 -clausify Defnoskolem pigeon.lp > out.tptpThe current version is completor-0.2.tar.gz. It is implemented in Python. Ply (Python Lex/Yacc) package is used and included in the download. You can also find the benchmark examples that are used in the paper.
O. Sabuncu, F. N. Alpaslan, Computing Answer Sets Using Model Generation Theorem Provers.
This version appeared in Proc. of the 4th Workshop on Answer Set Programming Advances in Theory and Implementation at the 23rd International Conference on Logic Programming, 2007.