Abstracts and scheduling for the CLAWS 2025 tutorials.
In my introduction to the winter school, I will present an up to date perspective on Computational Logic, defining what can be seen as it current goal and its importance, from a very personal perspective. I will introduce the different topics that will be covered in the School, and present the researchers that are joining this initiative.
This tutorial introduces two central meta-theorems of classical propositional logic: soundness and completeness. Soundness ensures that everything provable in a deductive system is semantically valid, while completeness guarantees that all semantic truths are provable. The focus will be on the proof strategy for completeness, highlighting the role of maximally consistent sets and their use in building models directly from syntactic properties. The aim is to clarify the connection between syntax and semantics in logic, and to provide participants with a basic ideas useful in broader logical settings.
One of the main focus of the school will be on modal logics, which can be seen as logics which are specially tailored for certain applications. In this tutorial I will introduce some of the basic tools to work with modal logics. I will discuss syntax and semantics of the basic modal logic, and some variants. Then, discuss some of their model theoretic and computational properties. To prepare for the invited talks during the second week of the school, I will then introduce dynamic modal logics, and explain why they are, nowadays, a hot topic of research.
This tutorial introduces tableaux-based techniques for reasoning in modal logic. It will explore how to construct systematic tableaux to decide satisfiability and validity, and explore how these methods provide an intuitive, algorithmic approach to modal reasoning.
This tutorial addresses the questions of what can be computed, how efficiently, and where the boundaries of solvability lie. It explores the foundations of computability and complexity, from Turing machines and the Church–Turing Thesis to central problems such as the Halting Problem, Satisfiability, and Model Checking. Key complexity classes including P, NP, and PSPACE will be introduced, with illustrative examples drawn from first-order and modal logics.
The so called formal methods for software development aim at guaranteeing software correctness, through the use of notations and mechanisms for software analysis based on solid mathematical grounds. These methods often employ logical notations in order to specify the expected behavior of software, and provide techniques to reason about the actual software behavior, and contrast it with the specification. While formal methods do offer stronger guarantees of software correctness, compared with the typical mechanisms for software validation and verification, there exist two classical issues that prevent their practical usage: the difficulty of capturing the expected behavior of software in a formal notation, and the problem of guaranteeing, once a specification is constructed, that the software satisfies the specification. These problems demand mastering the logical specification languages, as well as the deductive mechanisms associated with the languages. For this reason, the use of formal methods has been, for a long time, restricted to safety-critical software, where strong correctness guarantees are necessary, and therefore the cost of formal methods is justified.
In the last few decades, the above-described situation has changed substantially: formal methods have adapted and permeated multiple analysis techniques of broader adoption. Indeed, a diversity of formal techniques have overcome the previously mentioned issues, enabling practical applicability, but at the same time diminishing the correctness guarantees that they offer. These methods are called lightweight formal methods, and this talk will discuss a particular case: formal verification via SAT solving. SAT solving, the process of algorithmically determining if a propositional formula is satisfiable or not, has many applications in software engineering, and program verification is one of them. I will introduce the problem of software verification, how it can be tackled via SAT solving, and the main advantages and limitations of this approach. Finally, I will discuss the fundamental role of formal specification in the use of formal methods, and some more recent lines of research, that aim at assisting developers in the problem of formally describing the expected behavior of software.
In the last years there have been an increasing interest in languages to describe the dynamic evolution of a system. Classically, most formal approaches evaluate specifications over a static model. If the goal is to specify an evolving system, a temporal dimension is usually added and described using temporal operators. Dynamic logics propose, instead, to extend the expressive power of the formal language with operators that can change the model while we are evaluating the specification. In this tutorial I will introduce basic ideas on logics with dynamics operators that will help to understand Saturday’s tutorials.
This is a mini-course on graph games, a concrete model for a wide range of interactive scenarios, and the design of matching logical systems. Two particular meeting points in the past two decades are sabotage games and cops-and-robbers games, both inspiring new modal logics capturing game structure and players’ reasoning. The course introduces recent developments, reviews possible-world semantics, and—using cops-and-robbers as a case study—extends basic modal logic to account for concepts like “catching,” incorporating epistemic logic to examine uncertainty. The latter part explores how these modal logics relate to fragments of first-order and fixed-point logics, compares different logics for varying levels of game complexity, and connects with dynamic epistemic logic (DEL) for modeling dynamic information change.
This tutorial continues “Graph Games and Logic Design.” It focuses on graph games in which the underlying graphs can change, and on the formal properties of their matching logical systems. Two main dynamics are discussed: sabotage-style games (link modification) and poison games (state-property updates). These games model interactions between agents and have applications in areas such as abstract argumentation theory and graph theory. The session introduces logical systems matching these games, explores their properties, and outlines directions for future research.