Isolated Sublattices and
their Application to Counting Closure
Operators

Isolated sublattices are a special kind of sublattices which can serve to diminuish the number of elements of a lattice by means of a quotient lattice.

At the same time, there are simple formulae for the relationship between the number of closure operators in the original lattice and its quotient.

This connection can be used to derive an algorithm for counting closure operators, provided the lattice contains suitable isolated sublattices.

Second-Order Properties
of Undirected
Graphs

Time Warps, from Algebra to
Algorithms

Experimental
Investigation of Sufficient Criteria for Relations to Have
Kernels

Relational Computation
of Sets of
Relations

On Tools for
Completeness of Kleene Algebra with
Hypotheses

A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by reproving completeness of KAT and treat several other examples.

On Algebra of Program
Correctness and
Incorrectness

In this paper we describe an extension of Kleene algebra, an algebra with backwards diamond operators and countable joins for tests, which embeds IL, and which also is complete for reasoning about the image of the embedding. In addition to embedding IL, the algebra retains the ability to embed HL, and to make connections between IL and HL specifications: In this sense, it unifies correctness and incorrectness reasoning in one formalism.

Relation-algebraic
Verification of Borůvka's Minimum Spanning Tree
Algorithm

lr-Multisemigroups,
Modal Quantales and the Origin of
Locality

Relational Sums and
Splittings in Categories of L-fuzzy
Relations

Change of Base using Arrow
Categories

Abstract Strategies
and
Coherence

Relational Models for the
Lambek calculus with Intersection and
Unit

Free Modal Riesz Spaces
are Archimedean: a Syntactic
Proof

Some modal and temporal
translations of generalized basic
logic

A Variety Theorem for
Relational Universal
Algebra

Deciding
FO-definability of Regular
Languages

Accretive Computation of
Global
Transformations

The class of representable
semilattice-ordered monoids is not a
variety

Amalgamation property
for varieties of BL-algebras generated by one chain with finitely
many
components

Effect Algebras,
Girard Quantales and Complementation in Separation
Logic

Algorithmic
correspondence for relevance logics, bunched implication logics, and
relation algebras via an implementation of the algorithm
PEARL

In the present work, we re-interpret the algorithm PEARL from an algebraic perspective with its rewrite rules seen as manipulating quasi-inequalities interpreted over Urquhart's relevant algebras. This enables us to complete the part of the Sahlqvist theorem still outstanding from the previous work, namely the fact that all inductive RL formulas are canonical, i.e., are preserved under canonical extensions of relevant algebras. Via the discrete duality between perfect relevant algebras and Routley-Meyer frames, this establishes the fact that all inductive RL formulas axiomatise logics which are complete with respect to first-order definable classes of Routley-Meyer frames. This generalizes the "canonicity via correspondence" result in [Urquhart, 1996] for (what we can now recognise as) a certain special subclass of Sahlqvist formulas in the "groupoid" sublanguage of RL where fusion is the only connective. By extending RL with a unary connective for converse and adding the necessary axioms, our results can also be applied to bunched implication algebras and relation algebras.

We then present an optimised and deterministic version of PEARL, which we have recently implemented in Python and applied to verify the first-order equivalents of a number of important axioms for relevance logics known from the literature, as well as on several new types of formulae. In the paper, we report on the implementation and on some testing results.

Automated Reasoning
for Probabilistic Sequential Programs with Theorem
Proving

Domain Range Semigroups and Finite
Representations

Computing Least and Greatest Fixed
Points in Absorptive
Semirings

Our main result is a closed-form solution for least and greatest fixed points based on the fixed-point iteration. The proof builds on the notion of (possibly infinite) derivation trees; a careful analysis of the shape of these trees allows us to collapse the fixed-point iteration to a linear number of steps. The second method is an iterative symbolic computation in the semiring of generalized absorptive polynomials, largely based on results on Kleene algebras.

Polyadic spaces and profinite
monoids

Skew metrics valued in
Sugihara
semigroups

Any linear ordering on $X$ gives rise to an ordering on the set of its skew metrics valued on an arbitrary involutive residuated lattice $Q$. If $Q$ satisfies the mix rule, then this poset is most often a lattice. We study this lattice for $X = \{1,\ldots ,n\}$ and $Q$ the Sugihara monoid on the chain of cardinality $2K+1$. We give a combinatorial model of this lattice by describing its covers as moves on a appropriate space of words coding perfect augmented plane trees. Using the combinatorial model, we develop enumerative considerations on this lattice.

Unary-determined
distributive l-magmas and bunched implication
algebras

$\cdot$ is associative then $(A,\vee,\cdot)$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is \emph{unary-determined} if $x\cdot y=(x\top\wedge y)\vee(x\wedge \top y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations $p,q$. We obtain simple conditions on $p,q$

such that $x\cdot y=(px\wedge y)\vee(x\wedge qy)$ is associative, commutative, idempotent and/or has an identity element.

This generalizes previous results on the structure of doubly idempotent semirings and, in

the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic.

We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models.

Computing Aggregated
Knowledge as the Greatest Lower Bound of
Knowledge

We prove that for distributive lattices of size $n$, (1) the meet of join-endomorphisms can be computed in time $O(n)$. Previous upper bound was $O(n^2)$.

We show that (2) aggregated knowledge of given group can be viewed as the meet of the knowledge of each member of the group. We also show that for state sets of size $n$, (3) aggregated knowledge can be computed in time $O(n^2)$ in the general case and (4) for $S5$ knowledge (or \emph{Aumman structures}), it can be computed in time $O(n\alpha(n))$ where $\alpha(n)$ is the inverse of the Ackermann function.