Sequent Calculus and Query Sequent

Gen2Sat is a tool for deciding derivability in analytic propositional pure sequent calculi, by reducing it to classical satisfability. The reduction is based on the paper: SAT-based Decision Procedure for Analytic Pure Sequent Calculi, Ori Lahav, Yoni Zohar. Proceedings of IJCAR 2014. The source code and command-line utility can be downloaded here. The web interface was written using Framework, based on this example. rendering is done with . The SAT-solver that we use is sat4j . The tool was implemented by Yoni Zohar. Any comments or questions are welcome.