LOGI is a didactic tool designed for "Logica Matematica", a first year course of the "Corso di Laurea in Informatica" at the University of Milan. The decision of developing LOGI followed three years of experience using the course-ware associated to Language, Proof and Logic [1] (LPL, https://ggweb.gradegrinder.net/lpl). This is one of the most widely used logic course-ware: it is available since 2002 and includes, among other tools, "Tarski's World" (TW), which provides a virtual environment for students to draw on the screen virtual worlds populated by blocks (see Fig. 1); the aim is to learn the formal language of logic and understand its semantics in an easy and intuitive way.

"There are two ways to learn a second language. One is to learn how to translate sentences of the language to and from sentences of your native language. The other is to learn by using the language directly. . . . In LPL, we adopt the second method for learning FOL [first-order logic]. Tarski's World provides a simple environment in which FOL can be used in many of the ways that we use our native language. . . . With LPL, students learn not Fig. 1. A Tarski's World screenshot just how to prove consequences of premises, but also the equally important technique of showing that a given claim does not follow logically from its premises. To do this, they learn how to give counterexamples, which are really proofs of non-consequence. These will often [our emphasis] be given using Tarski's World" ([1], pages 14-5).

In our experience, TW effectively helps students in gaining some understanding of logic and students do like it. LPL contains a ton of exercises that can be developed and checked via the tools and we used them in lectures and as support for homework. However, most exercises involve signatures and interpretations different from TW. For example, there are exercises requiring to translate English statements into FOL, "introducing names, predicates, and function symbols as needed", considering other first order languages and interpretations, or asking to prove that an argument valid in TW is not valid in FOL, etc. These exercises have to be solved by hand. It will come to nobody's surprise that many students present very confused and imprecise solutions, which are in turn difficult to grade. Furthermore, students themselves would like to have a tool to check the correctness of their homework. LOGI aims to address those issues by: a) Defining first order (possibly many sorted) signatures, which can be stored and reused. b) Writing formulas and arguments in the language of a chosen signature. LOGI checks the correctness of formulas with respect to the signature. If no signature is declared, LOGI tries to infer one from the formulas. c) Introducing finite interpretations of the chosen signature. LOGI checks that interpretations are correctly formulated. d) Evaluating the truth/falsity of formulas in an interpretation or in a set of interpretations. LOGI shows also a detailed explanation of the computation of an evaluation. e) Supporting explicit definitions.

An additional motivation for LOGI is to emphasize the role of modeling in software development: FOL can be seen as a paradigmatic modeling language with a consolidated formal semantics. LOGI allows students to formalize "contexts", that is the set of "circumstances" which we are reasoning about. In LOGI a formal model of a context is obtained by introducing a signature that allows the user to represent all the circumstances of interest as first order interpretations and to express all related properties by primitively or explicitly defined symbols. Furthermore, to help modeling large examples, LOGI handles incomplete information, in the form of partially defined interpretations as well as of partially defined functions, corresponding to situations of partial knowledge typical of software systems. Note that since we also allow integers as a fixed structure, our system is outside of the strict limits of first-order logic. The first step is to create the required signature via the button "Crea Segnatura" in the "Creazione Fogli" menu (Fig. 2, left). Sheets are the basic units of the tool and an exercise involves the creation of a set of sheets of different kinds: .sig for signatures, .sp for formulas of a specific signature, .intp for interpretations and so on. Fig. 2, right, shows how to give a (many sorted) first order signature. A signature always includes u, the "universe" of discourse, while in this example we also have integers, used here to interpret the height function. In LOGI, by declaring the sort integer the predefined structure of integers is automatically included. If types in constant, function or predicate declarations are different from u, they have to be explicitly declared (see the declaration of height in Fig. 2); otherwise u is assumed. The syntax of declarations is quite intuitive and the tool clearly reports mistakes by highlighting.

The second step is to write down the required translations (Fig. 3). We consider here only two of the statements of the exercise, shown in the comments. Formulas are checked with respect to both FOL syntax and the declared signature. Once the formulas are correct, the sheet is accepted.

The third step is to formalize the required interpretation, a fragment of which is shown in Fig. 4. Mistakes, such as for example multi-valued functions, are signaled by error messages. In the case of partially defined information, the tool just issues a warning, see again Fig. 4. Finally, in exercises such as the one considered here, the last step is to evaluate the truth of formulas in a given sheet w.r.t. the considered interpretation. This is done via the "Esercizi" menu (details omitted). The result is Logically, this is accomplished recording during the interpretation, and then verbalizing evaluation forms [2], which are essentially a kind of realizers of given formulas.

The tool is entirely developed in SWI Prolog -LPL's Java code basis being proprietary -and consists of circa 6000 lines of code, including extensive comments. It contains three main "components": application, parser, and GUI, trying to bend SWI's limited module system to approximate as much as possible the notion of software components; this in order to separate the basic functionalities from the concrete representation of the sheets and from the GUI, simplifying future improvements and modifications. The information flow is the following: Sheet on the GUI ↔ (1) list(char) for the parser ↔ (2) Prolog term for the application The GUI is responsible for the translation (1). Different GUIs may behave in different ways, but all have to produce the same representation for the parser. The current GUI is based on XPCE-Emacs. For better rendering of logical symbols, we use different fonts and encodings for Windows and Unix systems. A custom written DCG parser, with a reasonable error messaging, is in charge of the translation (2). We refer to that as a "compilation".

Finally, the application component contains the basic functionalities. It defines the Prolog representation of signatures, interpretations and formulas, it checks the conformance of formulas and interpretations to a signature and evaluates the truth-value of formulas in an interpretation. Moreover, a compilation manager module maintains a dynamic database of the compiled sheets and their dependencies: for example, if a signature sheet is modified, the interpretation and formula sheets depending on it in general are no longer correct and thus are deleted from the compiled ones.