Equivalence Verification for Disjunctive Logic Programs

DLPEQ

[Background] [Examples] [References] [Using the software] [Download] [Back to LPEQ]

Background

The translator dlpeq is an implementation of the method for verification of weak equivalence of disjunctive logic programs in [OJ, LPNMR'04]. It is designed to be used with GnT and the front-end lparse (pre 1.0.14) which are available here. If you use lparse 1.0.14 or later, use dencode to switch to the old format.

Using the Software

dlpeq is used as follows in order to check the equivalence of program1.lp and program2.lp:

lparse --dlp program1.lp > program1.sm
lparse --dlp program2.lp > program2.sm

Either using one-phased or two-phased translation:

One-phased:

dlpeq program1.sm program2.sm | gnt 1
dlpeq program2.sm program1.sm | gnt 1

Two-phased:

dlpeq -p 1 program1.sm program2.sm | gnt 1
dlpeq -p 1 program2.sm program1.sm | gnt 1
dlpeq -p 2 program1.sm program2.sm | gnt 1
dlpeq -p 2 program2.sm program1.sm | gnt 1

More examples of the usage of dlpeq 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 binary is held by Emilia Oikarinen. You may freely use this software for academic and research purposes but not redistribute it.

dlpeq (version 1.9)

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

Latest update: 06 February 2013. Emilia Oikarinen