/Skeptik

A library for Proof Theory (especially Proof Compression) in Scala.

Primary LanguageScala

License Logo

Skeptik is a collection of data structures and algorithms focused especially on the compression of formal proofs.

Resolution proofs, in particular, are used by various sat-solvers, smt-solvers and automated theorem provers, as certificates of correctness for the answers they provide. These automated deduction tools have a wide range of application areas, from mathematics to software and hardware verification.

By providing smaller resolution proofs that are easier and faster to check, Skeptik aims at improving the reliability of these automated deduction tools and at facilitating the exchange of information between them.

###Usage Instructions###

Tell your java virtual machine to use UTF-8 and more memory. You can do this by setting your environment variable with the following command:

  $ export JAVA_TOOL_OPTIONS="-Dfile.encoding=UTF-8 -Xmx1024m -Xss4m -XX:MaxPermSize=256m"

(you may change the values after -Xmx, Xss and XX:MaxPermSize= to suit your needs)

You must have SBT (version >= 0.13) installed. SBT automatically downloads all compilers and libraries on which Skeptik depends.

To start SBT, go to Skeptik's home folder using the terminal and run:

  $ sbt

You can run skeptik within SBT's command line. With the following SBT command, skeptik will be compiled and executed, and a help message will be shown.

  > skeptik --help

The following command processes the proof 'eq_diamond9.smt2' using the algorithms 'RP' and the sequential composition of 'D', 'RPI' and 'LU'. The compressed proofs are written using the 'smt2' proof format.

  > skeptik -a RP -a (D-RPI-LU) -f smt2 examples/proofs/VeriT/eq_diamond9.smt2

To use skeptik from outside SBT, a jar file must be generated by executing the following command within SBT:

  > one-jar

The generated jar file can be deployed and used like any other java jar file:

  $ java -jar skeptik.jar -a RP -a (D-RPI-LU) -f smt2 examples/proofs/VeriT/eq_diamond9.smt2

###Skeptik as a Library###

To import Skeptik as a library in your own Java or Scala projects,
add the following line to your build.sbt file, if you are using SBT to manage the library dependencies of your project:

   libraryDependencies += "at.logic" %% "skeptik" % "1.0"

or add the following lines to your pom.xml file, if you are using Maven instead:

        <dependency>
            <groupId>at.logic</groupId>
            <artifactId>skeptik_2.10</artifactId>
            <version>1.0</version>
        </dependency>

###Stats###

Build Status Ohloh

###Development Policy###

Developers are encouraged to:

  1. fork from Paradoxika/Skeptik,
  2. program according to the usual Scala style conventions,
  3. follow the git flow branching model in their own forks,
  4. make pull requests when they have finished a feature or hotfix branch.

Using the git flow model can be easier with the gitflow extension for git.

###Documentation###

Detailed theoretical descriptions of some of the algorithms implemented in Skeptik are available in our papers. There are also slides of presentations about Skeptik.

Scaladoc documentation for the code can be generated by running the following command:

  sbt doc

###Active Developers###

Full list of contributors

###Job Opportunities###

###Communication Channels###

###Support###