Skeptik
A library for proof theory (especially focused on proof compression) in Scala.
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 installed. Then go to Skeptik's root directory using the terminal and simply execute:
sbt run
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
Authors and Contributors
Mailinglists
- skeptik-dev@googlegroups.com - for Skeptik's developers