LOGI: A didactic tool for a beginners' course in logic (system description)

LOGI is a didactic software designed for a basic course of Logic. We developed it as an extension of the course-ware Language, Proof and Logic (LPL) by Plummer, Barwise, and Etchemendy, in particular of Tarski's World (TW): The latter features simple virtual worlds populated by blocks and equipped with a first order language to about them; this helps students to understand the language of logic and its semantics in an intuitive and effective way. A limit is that there is no automatic support for exercises involving other domains. More importantly, if we view logic as a paradigmatic modeling lan-guage, this aspect is lost in the predefined blocks world, while it should be one of the educational outcomes of a course of Logic in a Computer Science curricu-lum. To overcome those limits, LOGI provides an environment where students can model simple ealities" by devising an appropriate (one-or many-sorted) signature, writing finite interpretations that represent possible circumstances, and evaluating the truth/falsity of first order formulas in an interpretation ac-cording to Tarski's semantics. Furthermore, it provides a detailed explanation of the result of evaluating a formula in a set of interpretations. Finally, to stress the role of logic in modeling, LOGI supports explicit definitions and allows the user to deal with incomplete information. In this sense, LOGI is not a com-petitor of TW, but an extension, to be used as a second, more advanced step.