The meta-interpreter supports tabled LP and coinduction.

• Tabled LP is supported following the DRA strategy of Guo and Gupta.
• Tabling and coinduction are used to develop an implementation of an LTL model checker.
• Example applications for the model checker are also included with the distribution.
• The whole system has been developed by Feliks Kluzniak at UT Dallas.

Download from here: http://www.utdallas.edu/~gupta/meta.tar.gz. Please send me an email at gupta@utdallas.edu, if you download the meta-interpreter.