From the logic of GK to disjunctive logic programs


gk2dlp is a system for computing models of (and thus reasoning with) theories of the (pure) logic of GK. The system translates such theories into disjunctive logic programs based on a Theorem by Jianmin Ji and uses disjunctive ASP solvers to compute models of the GK theories.

The gk2dlp system is written in ECLiPSe Prolog and implements the translation from GK theories to disjunctive logic programs presented in a recently submitted paper. It takes as input a representation of a pure theory of the logic of GK and transforms it into a propositional disjunctive logic program. The models of this logic program can then be computed by invoking an external ASP solver.


gk2dlp is distributed under the GNU General Public License. It has been developed and should run under ECLiPSe Prolog 6.0 on ubuntu 12.04 using claspD-2 as underlying disjunctive LP solver. You can download a package containing the source code along with some example theories.

More Information

Pure theories of the logic of GK are stored in text files with a special syntax. For example, the GK formula “Ap implies Kp” is represented by the Prolog fact implies(assume(p), know(p)).. A theory is represented by a collection of such facts for each formula in the theory. The remaining connectives and truth constants are expressed through and/2, or/2, iff/2, neg/1, true/0, false/0, and propositional atoms are represented by Prolog atoms.


gk2dlp is maintained by Hannes Strass. Feel free to contact him with any questions, comments or feedback.