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:

- The Natural Deduction Proof Checker (NDPC) tool (see its manual) for propositional and predicate logics developed by Brian Mulanda, Rodney R. Howell, and James Thompson.
- The Floyd-Hoare Programming Logic Proof Checker developed by Schmidt that accompanies his Programming Logics lecture notes.

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).

Robby

SAnToS Laboratory

Computing & Information Sciences Department

College of Engineering

Kansas State University

2181 Engineering Hall

1701D Platt Street

Manhattan, KS 66506

Phone: (785) 532-6350

Fax: (785) 532-7353

Email: robby@k-state.edu

SAnToS Laboratory

Computing & Information Sciences Department

College of Engineering

Kansas State University

2181 Engineering Hall

1701D Platt Street

Manhattan, KS 66506

Phone: (785) 532-6350

Fax: (785) 532-7353

Email: robby@k-state.edu