Gen2sat swMATH ID: 16745 Software Authors: Zohar, Yoni; Zamansky, Anna Description: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi. Gen2sat [1] is an efficient and generic tool that can decide derivability for a wide variety of propositional non-classical logics given in terms of a sequent calculus. It contributes to the line of research on computer-supported tools for investigation of logics in the spirit of the “logic engineering” paradigm. Its generality and efficiency are made possible by a reduction of derivability in analytic pure sequent calculi to SAT. This also makes Gen2sat a “plug-and-play” tool so it is compatible with any standard off-the-shelf SAT solver and does not require any additional logic-specific resources. We describe the implementation details of Gen2sat and an evaluation of its performance, as well as a pilot study for using it in a “hands on” assignment for teaching the concept of sequent calculi in a logic class for engineering practitioners. Homepage: http://gen2sat-yonizohar.rhcloud.com/gen2sat/ Related Software: MetTeL; Coq; intuit; GoedelGod; Archive Formal Proofs; smt; z3; SMT-LIB; KEMS; NESCOND; LoTREC; Sat4j; MUltlog Cited in: 3 Documents Cited by 5 Authors 2 Zamansky, Anna 2 Zohar, Yoni 1 Schmidt, Renate A. 1 Tishkovsky, Dmitry 1 Woltzenlogel Paleo, Bruno Cited in 0 Serials Cited in 2 Fields 2 Mathematical logic and foundations (03-XX) 2 Computer science (68-XX) Citations by Year