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 first-order 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###

You must have SBT (version >= 0.11.3) installed. Then go to Skeptik's root directory using the terminal and simply execute:

  export JAVA_TOOL_OPTIONS="-Dfile.encoding=UTF-8 -Xmx512m -XX:MaxPermSize=256m"

  sbt run

(you may increase the value after -Xmx, if you need or want to provide more memory to the JVM)

Further instructions, such as necessary command-line arguments, will be shown to you. If you face any difficulty, do not hesitate to contact us.

###Stats###

• 
• Ohloh

###Development Policy###

Skeptik developers and contributors are encouraged to:

1. fork from Paradoxika/Skeptik,
2. follow the git flow branching model in their own forks,
3. 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.

###Developers and Contributors###

• Bruno Woltzenlogel Paleo
• Joseph Boudou

###Websites and Forums###

• Skeptik's Main Website
• Skeptik's Mailinglist for Developers

###Support###

• Skeptik's development is currently funded by the Austrian Science Fund (Project P24300)
• Skeptik was supported by Google Summer of Code 2012
• YourKit is an excellent profiler for Scala applications. It supports our open-source project with a free license.