TCS / Software / lpeq
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Equivalence Verification of Logic Programs

LPEQ


[Background] [Examples] [References] [Usage] [Download] [Utilities - ASPtools] [Disjunctive programs - dlpeq]

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

lpeq is used as follows,
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
For instance, lpeq is used as follows in order to check the equivalence of program1.lp and program2.lp:
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

Disclaimer: The software below is provided on "as is" basis, without warranties of any kind or fitness for a particular purpose.

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-1.19
  • 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


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 06 February 2013. Tomi Janhunen