Warthog Logic

Warthog is a logical toolbox for propositional, first-order, higher-order, temporal and description logics. It is currently used in teaching automated reasoning courses at the University of Tübingen. Our vision is to produce a comprehensive framework for manifold logics and integrate external provers and knowledge compilation tools (e.g. SAT solvers, automated theorem provers, description logic reasoners, BDD packages, DNNF compilers, ASP environments, etc.). The goal is to represent and manipulate formulas in scala and then feed them to your tool of choice, thereby allowing to e.g. convert a general propositional formula to CNF, feed it to a SAT solver, then to a DNNF compiler, project the result to a subset of its variables and build a BDD out of it.