Browse Proceedings

We provide a set of syntactic tools for structuring large collections of logical theories. Their use is demonstrated by a formalisation of algebras that are used in describing the semantics of concepts in programming languages, but also of more general ...

We deliver a short overview of different centrality measures and influence concepts in socialnetworks, and present the relation-algebraic approach to the concepts of power and influence. First, we briefly discuss four kinds of measures of centrality: ...

Tableau-based deduction is an active and well-studied area of several branches of logic and automated reasoning. In this paper we discuss the challenge of automatically generating tableau calculi from the semantic specification of logics, while ...

Perhaps the most influential result in social choice theory is Arrow's impossibility theorem, which states that a seemingly modest set of desiderata cannot be satisfied when aggregating preferences [1]. While Arrow's theorem might appear rather negative,...

We present a new integration of relational and algebraic methods in the Isabelle/HOL theorem proving environment. It consists of a fine grained hierarchy of algebraic structures based on Isabelle's type classes and locales, and a repository of more than ...

What makes the field of social choice so fascinating is that it is full of complexities, assertions about the impossibility of doing what seems quite natural to do, and many mysteries. Adding to its allure is the importance of the topic; these mysteries ...

In this paper we present a language and first-order calculus for formal reasoning about relations based on the theory of allegories. Since allegories are categories, the language is typed in Church-style. We show soundness and completeness of the ...

We describe a simple computing technique for solving independence and domination problems on rectangular chessboards. It rests upon relational modelling and uses the BDD-based tool RelView for the evaluation of the relation-algebraic expressions that ...

We show how formally and systematically to develop a purely functional version of Warshall's algorithm for computing transitive closures by combining the unfold-fold technique, relation-algebra and data refinement. It is based on an implementation of ...

When reasoning within separation logic, it is often necessary to provide side conditions for inference rules. These side conditions usually contain information about variables and their use, and are given within a meta-language, i.e., the side ...

We define a class of structures - preference algebras - such that properties of preference relations can be expressed with their operations. We prove a discrete duality between preference algebras and preference relational structures.

Brown and Gurr have shown a relational representation theorem for quantales. Complete idempotent left semirings are a relaxation of quantales by giving up strictness and distributivity of composition over arbitrary joins from the left. We show a ...

A known generic strategy for handling large transition systems is the combined use of bisimulations and refinement. The idea is to reduce a large system by means of a bisimulation quotient into a smaller one, then to refine the smaller one in such way ...

Congruences of path algebras are useful in the definition and analysis of pathfinding problems, since properties of an algebra can be related to properties of its quotient. We show that this relationship can apply even when the algebraic objects ...

We propose axioms for 1-free omega algebra, typed 1-free omega algebra and typed omega algebra. They are based on Kozen's axioms for 1-free and typed Kleene algebra and Cohen's axioms for the omega operation. In contrast to Kleene algebra, several laws ...

We use well-known algebraic concepts like semirings and matrices to model and argue about Wireless Mesh Networks. These networks are used in a wide range of application areas, including public safety and transportation. Formal reasoning therefore seems ...

We present a formalisation in the dependently-typed programming language Agda2 of basic category and allegory theory, and of generalised algebras where function symbols are interpreted in a parameter category. We use this nestable algebra construction ...

We study a weak variant of omega algebra, where one of the usual star induction axioms is absent, in the context of recursive regular equations. We present abstract conditions for explicitly defining the omega operation and use them for proving an ...

We show that a class of automata modulo simulation equivalence forms a model of probabilistic Kleene algebra. We prove completeness of this model with respect to continuous probabilistic Kleene algebras. Hence an identity is valid in continuous ...

Relation algebra can be used to specify information systems and business processes. It was used in practice in two large IT projects in the Dutch government. But which are the features that make relation algebra practical? This paper discusses these ...

Problem statements often resort to superlatives such as in eg. ". . . the smallest such number", ". . . the best approximation", ". . . the longest such list" which lead to specifications made of two parts: one defining a broad class of solutions (the ...

That matrices of relations also obey the rules of relation algebra is well known. When a suitable ordering relation is given, partialities may be conceived as their lattice-continuous mappings -- corresponding to existential images which are often ...

Splitting atoms in a relation algebra is a common tool to generate new algebras from old ones. This includes constructing nonrepresentable algebras from representable structures. The known method of splitting atoms does not allow that bijections ...

Homogeneous relation algebra is an elegant calculational framework with many applications in computing science. In one application of relation algebra, called Ampersand, heterogeneous relation algebra is used as a specification language for business ...