OOPS: An S5n Prover for Educational Settings
Gert van Valkenhoef, Elske van der Vaart, Rineke Verbrugge · Electronic Notes in Theoretical Computer Science · 2010
We present OOPS , an open source, cross-platform, easy-to-run tableau prover for S5 n . 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.