`GnT`

`GnT`

is an experimental implementation of the stable model
semantics for disjunctive logic programs [Gelfond and Lifschitz,
1991]. Our implementation is based on an architecture consisting of
two interacting `smodels`

solvers
for non-disjunctive programs. One of the them is responsible for
generating as good as possible model candidates while the other checks
for minimality, as required from disjuctive stable models. Please
see [Janhunen et al., 2006] for details.

This program is to be compiled under the `smodels`

(versions 2.*) source distribution; and it
is to be used with the front-end `lparse`

.

- Disjunctive rules are written in the following syntax:
`a1|a2|a2 :- b1, b2, b3, not c1, not c2, not c3.`

- Also rules with variables can be used, but the front-end
`lparse`

performs an instantation for the rules using domain predicates like`d(.)`

below:`a(X)|b(X)|c(X) :- d(X). d(1..10).`

- Parametrized disjunctions (lparse versions 1.0.14 and later)
in the heads of rules are also supported:
`|a(X):d(X)|. d(1..4).`

- The stable models of a disjunctive logic program can be computed
by giving a command line like
`lparse --dlp disjunctive-program.lp | gnt2 0`

`0`

is replaced by a positive integer*n*, then the first*n*stable models are to be computed (if so many stable models exist). - Even
*partial stable models*can be computed by giving the the command line option`--partial`

for`lparse`

. - Similarly,
*regular models*can be computed by giving the command line option`-r`

for`lparse`

.

The author of the first version of GnT (also included as example4.cc in the smodels source distribution) is Patrik Simons. The version GnT1 (given below) is basically the orginal one -- only few lines of code have been added to handle command line options. The second version (GnT2.* below), which is a derivative of the first one, was developed by Tomi Janhunen to speed up computation.

This software is distributed under the GNU General Public License (available from Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA). In particular, as stated in the licence agreement, the software is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Source code: files for GnT1 (the first
version) and GnT2 (version 2.1) -- to be
placed and compiled (Makefile) in a
subdirectory of the smodels source directory
(such as `examples`

therein). Inline functions may cause
problems with some compilers (g++ series 3.* and 4.*). This problem
is fixed in the smodels 2.32 distribution.

Precompiled Linux binaries and a gzipped tar-archive of the sources are also available for your convenience: GnT1, GnT2.1, GnT2.1 for lparse-1.0.14 (and later), and GnT.tgz. It is also possible to switch between old (pre 1.0.14) and new formats using dencode.

T. Janhunen, I. Niemelä, D. Seipel, P. Simons, and J.-H. You.
*
Unfolding Partiality and Disjunctions in Stable Model Semantics.
*
ACM Transactions on Computational Logic,
7(1), 1-37, January 2006.
(Also in Proc. of KR 2000, 411-419).

M. Gelfond and V. Lifschitz.
*Classical Negation in Logic Programs and Disjunctive Databases*.
New Generation Computing, 9 (1991), 365-385.

J. You and L. Yuan.
*A three-valued semantics for deductive databases and logic programs*.
Journal of Computer Systems and Sciences, 49 (1994), 334--361.

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]

Latest update: 06 February 2013. Tomi Janhunen