Equivalence Verification of Logic Programs

LPEQ

Background

lpeq is an implementation of a translation-based method for verification of equivalence of logic programs in the input language of smodels system. A list of related publications can be found here. The translator lpeq is designed to be used with smodels (versions 2.*) and the front-end lparse which are available here. Currently lpeq covers a variety of equivalences proposed for logic programs: weak (or ordinary) equivalence, visible equivalence, strong equivalence and classical equivalence. Most recently, also the case of modular equivalence of smodels program modules is covered.

In addition to lpeq certain additional tools might be of help when using the translation-based method for verification of equivalence, and can be found here.

For the case of disjunctive logic programs use the translator dlpeq which can be found here.

Using the Software

usage: lpeq <options> <file1> <file2>

Command line options for lpeq are the following:

• -h or --help: print help message
• --version: print version information
• -v: verbose mode (human readable)
• -c: classical equivalence
• -s: strong equivalence; excludes option -c, but presumes classical equivalence to work.
• -m: modular equivalence; excludes options -c and -s,
• -i: generate input; presumes option -m

lparse program1.lp > program1.sm
lparse program2.lp > program2.sm
lpeq program1.sm program2.sm | smodels 1
lpeq program2.sm program1.sm | smodels 1

When given the option -c (resp. -s) lpeq produces a program for testing the classical (resp. strong) equivalence of the programs given as input. In this case, you have to invoke lparse (using only versions 1.0.11 and later) using the command line option -d all. When given the option -m lpeq produces a program (module) for testing the modular equivalence of the modules given as input. Option -i can be used to add an input generator to the module produced by lpeq.

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

Download

Copyright: The copyright for the binaries is held by Tomi Janhunen. You may freely use this software for academic and research purposes but not redistribute it.

Current version

• lpeq (version 1.19) enables translation-based verification of modular equivalence [OJ, ASP'07].

Old versions

• lpeq-1.17, more support for verification of visible equivalence, [JO, TPLP'07]
• lpeq-1.13, also for verification of strong and classical equivalence, [JO, LPNMR'04]
• lpeq-1.7, for verification of weak equivalence, [JO, JELIA'02]

Benchmarks and scripts

• Encodings and benchmarks for [OJ, ASP'07] and [OJ, submitted'08]:
  README; n-queens: gen-x.lp, gen-y.lp, check-1.lp, check-2.lp; Hamiltonian cycles: graph.lp, hc.lp, reached.lp, hc-candidate.lp; grounded modules: ASP07-benchmarks.tgz
• Shell scripts, encodings and seeds for [JO, TPLP'07]:
  general_test, general_times, lpeq, naive_test, naive, README
  queens-x1.lp, queens-x2.lp, queens-y.lp, knapsack.lp, color.lp, hc.lp, seeds.tgz
• Shell scripts and encodings for [JO, JELIA'02]]:
  queens_test, queens_times.sh, general_test, running_times.sh, naive.sh, README
  queens.lp, queens_choice.lp, color.lp, hc.lp