Mapping abstract reasoning: a Freinet-inspired approach to creative logic communication in secondary schools

The teaching of the mathematical foundations of computer science - in particular, mathematical logic - is frequently hampered by a high degree of abstraction, leading to disengagement and significant barriers to student comprehension. Traditional pedagogical approaches, often centred on passive instruction and formal definition, struggle to convey the dynamic applicability of these concepts. This paper explores a novel application of Célestin and Élise Freinet's pedagogy -- originally develop...

Growing HOLMS: a verified automated prover for Grzegorczyk logic in HOL light

This paper presents a certified theorem prover for Grzegorczyk logic (Grz) implemented in the general-purpose proof assistant HOL Light. Our prover builds on original HOL Light formalisations of modal adequacy for Grz with respect to finite partially ordered frames, and on the standard full and faithful translation of Grz into G{\"o}del--L{\"o}b logic (GL). This formalised embedding allows us to extend the range of modal systems supported by the HOLMS library for automated modal reasoning, an...

Ultrafilter extensions for Veltman semantics

In this paper, we present a first-order frame condition for interpretability logic and show that the condition is not modally definable. Yet, the frame condition holds both on ILM and on ILP frames and, hence, is of potential importance for the long-standing open problem about the interpretability logic of all reasonable arithmetical theories. In the light of the Goldblatt-Thomason Theorem, the modally inexpressible frame condition serves as motivation to develop ultrafilter extensions for in...

Lastre etrusche dipinte nella collezione del J. Paul Getty Museum