Sireum Logika is an open source pedagogical tool being developed at SAnToS Laboratory, Kansas State University to aid in teaching an introductory logics course in computer science (e.g., CIS 301: Logical Foundations of Programming). In addition, Logika also serves as a research vehicle for investigating program verification techniques.
The tool is accompanied by: (1) a set of course notes, which is an adaptation of the Programming Logics lecture notes written by David A. Schmidt, and (2) an Integrated Verification Environment (IVE) for Logika – LIVE, built on top of JetBrains‘ IntelliJ IDEA. Logika uses the Z3 theorem prover to automatically solve algebraic formulae and to offer some level of automation suitable for an introductory logics course.
Logika is inspired by:
Logika is a combination of both tools; it uses the same input language for reasoning about propositional, predicate, and programming logics (i.e., the propositional logic language is a subset of the predicate logic language, which in turn, is a subset of the programming logic language). The programming logic language itself is a subset of the Scala programming language, whose programs can be run by using the regular Scala interpreter equipped with the Logika runtime library (maven).