| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 421888 | Electronic Notes in Theoretical Computer Science | 2010 | 13 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
