Events

Our inaugural meeting took place on 5th January 2023 from 12-14 in TG23. We have since had a very active number of bi-weekly lunchtime (byos) meetings and they are ongoing with the new meeting time Thursday 2.30-3.30 pm in TG23.

Please contact the convenor f.kammueller “at” mdx.ac.uk for details — also if you want to contribute by presenting your work.

If you are interested to join any of the meetings just turn up to TG23 on the date OR join the Zoom meeting below.

Join Zoom Meeting
Meeting ID: 910 2407 9295 Passcode: seta

Winter-Spring term 2025 meetings from Jan 2025

  • On 10th April Andrew Lewis-Smith presents Correspondence Theory for Intuitionistic Lukasiewicz logic Abstract: In the present paper, we develop the correspondence theory for intuitionistic {\L}ukasiewicz logic. We adopt the method of algorithmic correspondence theory, identify the class of inductive formulas, and develop an algorithm for computing the first-order correspondents of given inductive formulas. The key step is to find the interpretations of nominals and conominals, whose interpretations are the counterparts of singletons and their complements in intuitionistic {\L}ukasiewicz logic which can be translated into First-order Lukasiewicz logic.

    • Autumn 2024 meetings from September 2024

  • On 29th November Florian Kammueller presents Security Engineering in the Isabelle Insider and Infrastructure framework Abstract: We present an approach to developing secure system specifications for IoT systems with decentralized data in Isabelle. The Isabelle Insider and Infrastructure framework (IIIf) supports formalisation and proof of infrastructures with actors and policies and comes with the Refinement-Risk cycle (RR-cycle), a method for security engineering. The RR-cycle enables interleaving attack analysis with system refinement using rigorous machine assisted proof in Isabelle to scrutinize and refine system specifications until security requirements are met. We illustrate and motivate this approach by a couple of case studies. The first case study is motivated by the IoT project SUCCESS on security and privacy of healthcare IoT applications. We specify and analyse a privacy critical scenario by refining it with a distributed ledger. We further sketch the security specification and verification of air traffic control systems in the IIIf. Here, we present the extension of the IIIf by a formal notion of indistinguishability and prove the central noninterference property for flight path monitoring. This talk has been presented recently at University of Exeter as an invited CS Dept Colloquium.
  • On 25th October in a Joint SETA/Department Colloquium from 4-5pm in TG23, Andrew Lewis-Smith presents Constructive and Intermediate Fuzzy Logics
    Abstract: We present recent work developing relational semantics for Fuzzy / substructural logics. This work takes algebraic representation results of residuated lattices and extracts a generalisation of Kripke’s Famous semantics for Intuitionistic logic and extensions (alias Intermediate logics), to fuzzy analogues such as GBLewf (aka Intuitionistic Lukasiewicz logic) and Hajek’s BL. Our current work looks at a couple of special cases which are particularly interesting, namely Intuitionistic Lukasiewicz logic with Weak Excluded Middle and what we term Fuzzy Smetanovich logic. The non-fuzzy variants of these systems have connections to logic programming and computability theory, raising questions about what a fuzzy theory of computability look like.
  • On 23d September, Can Baskent presented Playing Games with Diagrams: Truth Diagrams and Game Semantics
    Can received the BEST PAPER AWARD at DIAGRAMS 2024! paper available online
    Abstract: In this paper we discuss the connection between truth diagrams and game semantics. Truth diagrams offer a diagrammatic way to represent truth in propositional logic. Game semantics, on the other hand, offers a strategic and game theoretical way to establish the truth value of a given formula. By establishing a relation between the two, we offer another diagrammatic reasoning for game semantics, beyond game trees; and characterise various operations on truth diagrams game theoretically. This paper has been presented in Diagrams 2024 conference.

    • Spring/summer meetings (May–July 2024)

  • On 20th May, Can Baskent presents A Logic of Isolation(slides)
    Abstract: In the vein of recent work that provides non-normal modal interpretations of various topological operators, this paper proposes a modal logic for a spatial isolation operator. Focussing initially on neighborhood systems, we prove several characterization results, demonstrating the adequacy of the interpretation and highlighting certain semantic insensitivities that result from the relative expressive weakness of the isolation operator. We then transition to the topological setting, proving a result for discrete spaces. It is a joint work with David Gilbert (University of British Columbia, Canada) and Giorgio Venturi (University of Pisa, Italy). The work will be presented at the WOLLIC conference in June.
  • On 3rd June, Florian Kammueller reports on GISMO proposal, DT Annual WS, and the recent VeTTS meeting
  • On 24th June (new date!), Giacomo Nalli presents Online Application for early identification of failure through artificial intelligence
    Abstract: A worrying trend that recently affected the university system is characterized by the students’ drop-out. Universities usually associate the problem with some aspects such as the study programme, the structure, and the organisation of the examinations, which require more involvement from students and negatively affect their motivation. Even when universities implement some improvement actions, such as tutoring, to provide students with the best possible approach to their studies, with the aim of promoting academic success and preventing university drop-out, they sometimes don’t seem to achieve the expected results. It can happen that the factors that led students to drop-out are not related to their approach to study, but to their engagement and social interaction. Universities find out about these factors only after students have dropped out, checking their activities and attendance only at the end of the academic year, too late for avoiding serious consequences. This work reports on a possible solution to this problem by using artificial intelligence methods based on machine learning, firstly by applying clustering to group students according to their behaviour and then by implementing a classification model to predict students at risk. Once checked the accuracy of the machine learning models, the application designed and implemented in this work has been plugged in an online platform to allow the university staff to easily run the software to support the students in achieving their goals in terms of engagement and learning outcomes.

  • Past meetings 2023