2026-09-30

Semantics of various formalisms in knowledge representation can be described by fixpoints of corresponding operators. For example, in many logics (e.g. propositional or modal logics) theories are fixpoints of the underlying consequence operator. Likewise, in logic programming, default logic, or formal argumentation, all the major semantics can be formulated as different types of fixpoints of the same operator.

Such operators are often non-monotonic, and so their fixpoints cannot be guaranteed to exist, or be defined constructively. In order to deal with this illusive nature of the fixpoints, Denecker, Marek and Truszczyński introduced a method for approximating each value z of the underlying operator by a pair of elements (x, y). These elements represent lower and upper bounds on z, and so a corresponding approximation operator for the original, non-monotonic operator, is constructed.

A natural requirement is that the approximating operator is precision-monotonic, intuitively meaning that more precise inputs of the operator give rise to more precise outputs. This requirement ensures (by Tarski and Knaster’s Fixpoint Theorem) that the approximating operator has fixpoints that can be constructively computed, and approximate the fixpoints of the approximated operator (whenever such fixpoints exist). Many existing formalisms in knowledge representation where shown to make implicit use of approximation fixpoint theory (e.g. logic programming, default logic, autoepistemic logic, abstract dialectical frameworks, hybrid MKNF, SCHACL, and active integrity constraints), and the semantics of several new formalisms were obtained by a straightforward application of approximation fixpoint theory (e.g. extensions of logic programs, weighted abstract dialectical frameworks (ADFs), access control policies and second-order logic extended with non-monotone inductive definitions).

In this talk, I will survey the main ideas behind this theory, and explain some recent advances, such as the extension of the theory to non-deterministic constructs such as disjunction and choice rules. This emphasis will be achieved by a detailed study of some of the formalisms to which the application of approximation fixpoint theory has received, historically, the most attention, namely logic programming.

t.b.a.

Multiparty session types (MPST) provide a rigorous foundation for verifying the safety and liveness of concurrent systems. However, existing approaches often force a difficult trade-off: classical, projection-based techniques are compositional but limited in expressiveness, while more recent techniques achieve higher expressiveness by relying on non-compositional, whole-system model checking, which scales poorly.

This paper introduces a new approach to MPST that delivers both expressiveness and compositionality, called the synthetic approach. Our key innovation is a type system that verifies each process directly against a global protocol specification, represented as a labelled transition system (LTS) in general, with global types as a special case. This approach uniquely avoids the need for intermediate local types and projection.

We demonstrate that our approach, while conceptually simpler, supports a benchmark of challenging protocols that were previously beyond the reach of compositional techniques in the MPST literature. We generalise our type system, showing that it can validate processes against any specification that constitutes a 'well-behaved' LTS, supporting protocols not expressible with the standard global type syntax. The entire framework, including all theorems and many examples, has been formalised and mechanised in Agda, and we have developed a prototype implementation as an extension to VS Code.