OOPS: An S5n Prover for Educational Settings

We present OOPS, an open source, cross-platform, easy-to-run tableau prover for S5n. OOPS is aimed at education in modal logics. Thus, it has several features that enable insight into its internal workings. Specifically, OOPS allows tableaux to be visualized and can generate counter-models for formulas that are not provable. Moreover, the OOPS Graphical User Interface (GUI) increases ease of use and an integrated general purpose scripting language (Lua) is used to provide convenient and powerful interactions with the OOPS tableau generator.