periplo

Proof tRansformer and Interpolator for Propositional LOgic

Intro

PeRIPLO is an open-source SAT-solver that features resolution proof manipulation and interpolant generation capabilities.

This page is the SVN source code repository for PeRIPLO (click Source tab).

Sources can be download using:

svn checkout http://periplo.googlecode.com/svn/trunk/ periplo

Also you need to install the following software: * gcc/g++ version >= 4.3.2 * autotools * libtool * flex * bison * zlib

(for Ubuntu users sudo apt-get install autoconf libtool g++ bison flex zlib1g-dev).

In addition you need to install The GNU MP Bignum Library.

More details on building PeRIPLO are available from wiki page BuildPeRIPLOFromSources.

Tutorials on how to use PeRIPLO can be found at Tutorial.

A choice of executables is available in the Downloads section.

If you find bugs please report them to us (using the Issues tab).

What you get from SVN. PeRIPLO is in continuous development.

GNU GPL version 3.

We wish to thank dr. Roberto Bruttomesso for his notable work on the SMT-solver OpenSMT, from which PeRIPLO was born.

The project was created on Apr 17, 2013.