Translating Circumscription to Disjunctive Logic Programming:

CIRC2DLP

News

• circ2dlp-2.1, a bugfix for version 2.0 (April 5, 2007)
• circ2dlp-2.0 now uses a linear translation from prioritized circumscription to disjunctive logic programs. (March 19, 2007)
• A set of diagnosis benchmarks used in [OJ, 2007] available (March 19, 2007)

Using the Software

usage: circ2dlp <options> <file> [-m <minimized:different:priorities> -v <varying> -f <fixed>]

Default behaviour is that all atoms are falsified with the highest priority, unless explicitly given a priority for minimization or stated to be varying or fixed. Different priorities are separated with a colon, and a lower priority for a certain atom overrides a higher one (see here for examples). Default behaviour can be changed using option --vary. Notice however, that invisible atoms that lparse produces (atoms that have no name in the symbol table) always have the default behaviour being minimized with highest priority and --vary option cannot be applied to programs containing invisible atoms, as the semantics of invisible atoms becomes unclear. Wildcards can be used when giving the set of minimized, varying and fixed atoms or predicates: ? matches any one character, * any character or characters and [ ] one of the characters included inside the brackets.

• -h or --help -- print help message
• -t -- human readable output
• --dlv -- output in dlv syntax
• --vary -- vary all atoms by default
• --version -- print version information

circ2dlp can also be used to programs containing negation. Then the translation yields the ⟨P_1>...>P_k,V,F⟩ -minimal models of the Gelfond-Lifschitz reduct of the original program Π, that is, the ⟨P_1>...>P_k,V,F⟩-stable models of Π in a sense.

lparse --dlp program.lp > program.sm
circ2dlp program.sm -v [atoms in V] -f [atoms in F] | gnt 0

circ2dlp --dlv program.sm -v [atoms in V] -f [atoms in F] | dlv -n=0 --

More examples of the usage of circ2dlp can be found here.

Download

Copyright: The copyright for circ2dlp is held by Emilia Oikarinen and for dencode, lpcat and lplist by Tomi Janhunen. You may freely use this software for academic and research purposes but not redistribute it.

Current version

• circ2dlp (version 2.1)

circ2dlp-2.1 has been designed to be used with GnT (version 2.1 for lparse-1.0.14) and the front-end lparse (version 1.0.14 or later). In addition, there is a support for producing an input file for dlv.

Old versions

• circ2dlp-2.0, a preliminary version of the linear translation for prioritized circumscription.
• circ2dlp-1.1 is designed to be used with GnT (version 2.1) and lparse (pre 1.0.14). Note that it is possible to switch between old (pre 1.0.14) and new formats using dencode.
• Version 1.1 has no direct support for prioritized circumscription. Lifschitz' scheme is implemented as a script prio_circ2dlp (README).
  • lpcat (concatenates two programs, version 1.5)
  • lplist (outputs program in textual format, version 1.3)

Benchmarks

• A set of diagnosis benchmarks used in [OJ, 2005]
• A set of diagnosis benchmarks used in [OJ, 2007] (README).

Troubleshooting

• lparse-1.0.17 produces warning messages of the form

  2: Warning: 0: lower bound (-2147483647) in an extended rule section is bigger than the upper bound (135097400)

  There are spurious warnings and can be neglected. A way to get rid of these messages is to use the -Wnone option of lparse-1.0.17.

• The newest versions of lparse (1.0.14 and higher) produce disjunctive rules with a new code (number 8) which is not understood by GnT. This results in error messages

  gnt2: error in input

  Therefore circ2dlp should be used with a special compilation of GnT for lparse 1.0.14 .

• circ2dlp (2.0 and higher) assumes input in the new lparse format, and circ2dlp (1.1) in the old format. If the input file for circ2dlp is in the wrong format, it results in an error message:

  circ2dlp: unknown rule type.

  This can be circumvented with the help of dencode which switches between old (pre 1.0.14) and new (1.0.14 and higher) formats of lparse (options -o and -n).